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...

• Type: Conference
• Year: 2005
• Where: HVC
• Authors: Zurab Khasidashvili, Alexander Nadel, Amit Palti, Ziyad Hanna
• Keywords: HVC 2005, Model Checking, Propositional Satisfiability, SSAT Algorithm