Last version:
The folder CMC_CPL.zip contains the MVS-project (composed by seven modules) that is reported in the paper:
Verified Model Checking for Conjunctive Positive Logic.
Alex Abuin, Unai Diaz de Cerio, Montserrat Hermo, Paqui Lucio and Rustan Leino.
Submitted to a Journal.
Old version:
The folder QCSP-Proof-System-Project-v6.rar contains the formalization (composed by four modules) of the QSCP-proof system on which we report in:
Towards the Automatic Verification of QCSP Tractability Results.
Alex Abuin, Hubie Chen, Montserrat Hermo, and Paqui Lucio.
In (ed): Proceedings XVII Jornadas sobre Programación y Lenguajes (PROLE 2017), Tenerife, Spain, 19-21 Julio 2017.