×

Simultaneous SAT-based model checking of safety properties. (English) Zbl 1176.68125

Ur, Shmuel (ed.) et al., Hardware and software verification and testing. First international Haifa verification conference, Haifa, Israel, November 13–16, 2005. Revised selected papers. Berlin: Springer (ISBN 3-540-32604-9/pbk). Lecture Notes in Computer Science 3875, 56-75 (2006).
Summary: 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 we can solve several other SAT objectives when the search is oriented to solve a particular SAT objective first. Experimental results on Intel designs demonstrate that our new algorithms can be orders of magnitude faster than the previously known techniques in this domain.
For the entire collection see [Zbl 1097.68009].

MSC:

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

Software:

SATIRE
PDFBibTeX XMLCite
Full Text: DOI