SAT-Based Model Checking without Unrolling

By Aaron R. Bradley. International Conference on Verification, Model Checking and Abstract Interpretation, 2011

815 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.

The nuXmv Symbolic Model Checker (2014, methodology): “On the left we compare IC3 with implicit abstraction algorithm [21] as available in NUXMV against state-of-the-art engines on a set of bit-vector (BV) benchmarks (we took all the benchmarks used in [20], using BV as background theory instead of LRA, the instances of the bitvector set of the Software”
Learning Shape Analysis (2017, background): “) is combined with a variation of the IC3 property-directed reachability algorithm [8] to prove memory safety and data properties.”
ZEUS: Analyzing Safety of Smart Contracts (2018, background): “The strength of the CHC representation enables it to interface with a variety of SMTbased solvers and off-the-shelf model checkers [56], [63].”
Efficient implementation of property directed reachability (2011, methodology): “More recently, another novel method was pioneered by Aaron Bradley [1, 2].”