Checking Safety Properties Using Induction and a SAT-Solver

By M. Sheeran, Satnam Singh, G. Stålmarck. Formal Methods in Computer-Aided Design, 2000

826 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Electrical and Electronic Engineering, Hardware and Architecture

View Paper: https://www.semanticscholar.org/paper/f73226d674fdaf5b86f3b03873971af5fc0a19f5

How researchers see this paper

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

In Computational Theory and Mathematics

In Electrical and Electronic Engineering

In Hardware and Architecture

Citations in the corpus

Contracts for System Design (2018, methodology): “Examples are the Scade Suite Design Verifier7 and Simulink Design Verifier [248], which are both based on the Prover Technology proof engine [239, 240], the products of PikeTec8 such as TPT, the tool AGATHA [55] developed at CEA/LIST and Uppaal [34] with its derivatives like Uppaal TIGA [77] and ECD”
Bounded model checking (2003, methodology): “Techniques based on induction can be used to make BMC complete for safety properties [25].”
Applying SAT Methods in Unbounded Symbolic Model Checking (2002, methodology): “Finally, another approach to using SAT in model checking is based on unfolding the transition relation to the length of the longest “shortest path” between two states [15].”
The nuXmv Symbolic Model Checker (2014, methodology): “Similarly to the finite case, we provide an SMT based implementation for the McMillan approach [5], the interpolation sequence approach [6], k-induction [7] and for algorithms based on IC3 [20,21].”
SAT-Based Model Checking without Unrolling (2011, methodology): “To investigate this question, we selected eight benchmarks from the competition that are diﬃcult but possible for the non-parallel version: Intel benchmarks 20, 21, 22, 23, 24, 29, 31, and 34.”
Interpolation and SAT-Based Model Checking (2003, background): “Another approach is based on unfolding the transition relation to the length of the longest simple path between two states [22].”
Software model checking (2009, positive): “One promising approach is k-induction [Sheeran et al. 2000; de Moura and Rueß 2003], which checks the inductiveness condition not for an edge (`, `′) but for paths of length k.”
Model checking (2009, neutral): “Other ways for making BMC complete are based on cube enlargement, 36 circuit co-factoring, 26 induction, 42 and Craig interpolants.”