Kember, MitchellTran, LynnGao, GeorgeDay, Nancy2020-06-162020-06-162019https://doi.org/10.1109/MiSE.2019.00015http://hdl.handle.net/10012/15994© 2019 IEEEWe 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, symbolic model checking method. As a CTL model checking method, TCMC is defined over transition systems and states (rather than paths) and therefore, returns a transition system with a bug as a counterexample. Our contribution is to isolate a counterexample path/subgraph in a declarative manner by adding constraints that do not depend on the property. Our method does not require extensions to Alloy.enmodel checkingcounterexamplessubgraphsTCMCCTLFCformal verificationtemporal logictransitive-closure-based model checkingCTL with fairness constraintssymbolic model checkingCTL model checkingcounterexamples extractionCTLFC model checkingfirst-order logic with transitive closuretemporal logic propertyAlloyAlloy AnalyzerConference Paper