SAT-based induction for temporal safety properties

MaRDI QIDQ2849589zbMATH OpenFDO

Authors Roy Armoni, Limor Fix, Ranan Fraer, Scott Huddleston, Nir Piterman, Moshe Y. Vardi

Publication date 20 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105000873

Mathematics Subject Classification ID

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

Recommendations

• Temporal induction by incremental SAT solving
• Induction in compositional model checking
• Hardware and Software, Verification and Testing
• Formal verification of Pentium^4 components with symbolic simulation and inductive invariants
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)

Cited in

(6)

• Indentification of inductive properties during verification of synchronous sequential circuits
• Temporal induction by incremental SAT solving
• SAT-Based Synthesis Methods for Safety Specs
• Automatically validating temporal safety properties of interfaces
• Formal verification of Pentium^4 components with symbolic simulation and inductive invariants
• Property-directed incremental invariant generation

This page was built for publication: SAT-based induction for temporal safety properties

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