Last version:


The folder 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.

[Electronic Edition]