QCTL model-checking

qctlmc: a tool for QCTL model-checking

qctlmc is a prototype: it is under development !
It is developped by:
It is a Python3 program which builds a QBF formula (for a QBF solver) from a Kripke structure and a QCTL formula.
QCTLMC provides a QBF formula in QCIR format (for cqesto, qfm, qfun, ghostq) or in Z3 format. To use QCTLMC, you have to install at least one of these solvers !
The new version of QCTLMC uses PLY package: here.

How to get qctlmc ?

NEW VERSION (February 15th, 2020): here.

Old version (only for Z3, June 2019): here.

Related papers:

About the reduction from QCTL to QBF: About QCTL:

Email: francois.laroussinie[at]irif.fr