Sciweavers

HVC
2005
Springer

Simultaneous SAT-Based Model Checking of Safety Properties

13 years 9 months ago
Simultaneous SAT-Based Model Checking of Safety Properties
We present several algorithms for simultaneous SAT (propositional satisfiability) based model checking of safety properties. More precisely, we focus on Bounded Model Checking and Temporal Induction methods for simultaneously verifying multiple safety properties on the same model. The most efficient among our proposed algorithms for model checking are based on a simultaneous propositional satisfiability procedure (SSAT for short), which we design for solving related propositional objectives simultaneously, by sharing the learned clauses and the search. The SSAT algorithm is fully incremental in the sense that all clauses learned while solving one objective can be reused for the remaining objectives. Furthermore, our SSAT algorithm ensures that the SSAT solver will never re-visit the same sub-space during the search, even if there are several satisfiability objectives, hence one traversal of the search space is enough. Finally, in SSAT all SAT objectives are watched simultaneously, thus...
Zurab Khasidashvili, Alexander Nadel, Amit Palti,
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where HVC
Authors Zurab Khasidashvili, Alexander Nadel, Amit Palti, Ziyad Hanna
Comments (0)