Searching for i-good lemmas to accelerate safety model checking

DOI10.1007/978-3-031-37703-7_14zbMATH Open1545.68076MaRDI QIDQ6535540FDOQ6535540

Authors: Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu 

Publication date: 12 January 2024

Recommendations

• Understanding IC3
• Generalized property directed reachability
• Property directed abstract interpretation
• Syntax-guided synthesis for lemma generation in hardware model checking
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Theory and Applications of Satisfiability Testing
• Interpolation and SAT-based model checking.
• SAT-Based Model Checking without Unrolling
• Evaluating CDCL variable scoring schemes
• SMT-based scenario verification for hybrid systems
• Interpolating strong induction
• Congruence \(ABC\) implies \(ABC\)

This page was built for publication: Searching for i-good lemmas to accelerate safety model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535540)