Extracting counterexamples from transitive-closure-based model checking
Proceedings of the 11th International Workshop on Modelling in Software Engineerings, pp. 47-54, 2019.
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
Full Text (Upload PDF)
PPT (Upload PPT)