Counterexample-preserving reduction for symbolic model checking
Summary: The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In such reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique ``counterexample-preserving reduction (CPR, for short), and the proposed technique is evaluated by conducting comparative experiments of BDD-based model checking, bounded model checking, and property directed reachability-(IC3) based model checking.
- Formal Methods in Computer-Aided Design
- scientific article; zbMATH DE number 1705164 (Why is no real title available?)
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 1979554 (Why is no real title available?)
- scientific article; zbMATH DE number 2086516 (Why is no real title available?)
- Linear Encodings of Bounded LTL Model Checking
- SAT-Based Model Checking without Unrolling
- Symbolic model checking: \(10^{20}\) states and beyond
- Theoretical aspects of computing -- ICTAC 2013. 10th international colloquium, Shanghai, China, September 4--6, 2013. Proceedings
- Understanding IC3
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Counterexample-preserving reduction for symbolic model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2336646)
