{"id":"arxiv/2608.24320","url":"https://arxiv.org/abs/2608.24320","tags":["cs.LO","quant-ph"],"score":0,"title":"QisMC: A Model Checker for QISKIT Program Debugging","domain":"cs.LO","source":"arxiv","authors":["Aochu Dai","Mingsheng Ying"],"reviews":0,"subject":"cs.LO","summary":"We present QisMC, the first quantum model checker dedicated to debugging Qiskit programs. On the theoretical side, we introduce the notion of quantum-classical transition system and a quantum computation tree logic (qCTL) grounded in Birkhoff-von Neumann logic for modeling the behaviors and specifying the properties of Qiskit programs, respectively. On the implementation side, QisMC provides an end-to-end framework encompassing transition system generation, logical formula representation, and model checking algorithms, and it efficiently performs image computation based on decision diagrams.…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-08-25","reactions":{}}