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
• scientific article; zbMATH DE number 1670785
• Hardware and Software, Verification and Testing
• Computer Aided Verification
• 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
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• Computer Aided Verification
• 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)