Extracting Counterexamples from Transitive-Closure-Based Model Checking
MetadataShow full item record
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, 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.
Cite this version of the work
Mitchell Kember, Lynn Tran, George Gao, Nancy Day (2019). Extracting Counterexamples from Transitive-Closure-Based Model Checking. UWSpace. http://hdl.handle.net/10012/15994
Showing items related by title, author, creator and subject.
Fallahi, Narges (University of Waterloo, 2014-08-08)A self-stabilizing protocol is one that starting from any arbitrary initial state recovers to legitimate states in a finite number of steps, and once it stabilizes to a set of legitimate states, it remains there unless it ...
Montaghami, Vajihollah (University of Waterloo, 2017-02-01)Models, especially those with mathematical or logical foundations, have proven valuable to engineering practice in a wide range of disciplines, including software engineering. Models, sometimes also referred to as logical ...
Vediramana Krishnan, Hari Govind (University of Waterloo, 2019-08-14)Symbolic Model checking is a widely used technique for automated verification of both hardware and software systems. Unbounded SAT-based Symbolic Model Checking (SMC) algorithms are very popular in hardware verification. ...