Applying SAT Methods in Unbounded Symbolic Model Checking

By Kenneth L. McMillan. International Conference on Computer Aided Verification, 2002

401 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Handbook of Satisfiability (2021, background): “In SAT, the problem of finding small unsatisfiable cores has been addressed by many authors in recent years [95, 103, 159, 116, 82, 58, 29, 74, 156] due to its importance in formal verification [100].”
Resolve and Expand (2004, background): “Another general bottom-up approach [16,14,15,6] is also based on quantifier elimination.”
Model Checking and the State Explosion Problem (2011, methodology): “Other techniques for making BMC complete are cube enlargement [18], circuit co-factoring [14], and Craig interpolants [19].”
Bounded model checking (2003, methodology): “McMillan [21] recently introduced a SAT-based unboundedCTL model checker.”
SAT-Based Model Checking without Unrolling (2011, methodology): “SAT-based unbounded model checking constructs clauses via quantiﬁer elimination; for a safety property P , it computes the weakest inductive strengthening of P [20].”