Extracting counterexamples from transitive-closure-based model checking

Mitchell Kember
Mitchell Kember
Lynn Tran
Lynn Tran
George Gao
George Gao

Proceedings of the 11th International Workshop on Modelling in Software Engineerings, pp. 47-54, 2019.

Cited by: 2|Bibtex|Views18|DOI:https://doi.org/10.1109/MiSE.2019.00015
EI
Other Links: dl.acm.org|dblp.uni-trier.de|academic.microsoft.com

Abstract:

We address the problem of how to extract counterexamples for the transitive-closure-based model checking (TCMC) technique. TCMC is a representation of the CTLFC (CTL with fairness constraints) model checking problem in first-order logic with transitive closure (FOLTC) and has been implemented in the Alloy Analyzer. It is a declarative, sy...More

Code:

Data:

Your rating :
0

 

Tags
Comments