Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11678779_5 | Haifa Verification Conference |
Keywords | Field | DocType |
sat objective,simultaneous sat,model checking,satisfiability objective,simultaneous sat-based model checking,search space,particular sat,safety property,ssat algorithm,propositional satisfiability,propositional objective,ssat solver,satisfiability | Constraint satisfaction,Discrete mathematics,Model checking,Tree traversal,Computer science,Satisfiability,Algorithm,Propositional calculus,Theoretical computer science,Conjunctive normal form,Solver,Bounded function | Conference |
Volume | ISSN | ISBN |
3875 | 0302-9743 | 3-540-32604-9 |
Citations | PageRank | References |
11 | 0.57 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Zurab Khasidashvili | 1 | 307 | 25.40 |
| Alexander Nadel | 2 | 213 | 13.95 |
| Amit Palti | 3 | 31 | 2.02 |
| Ziyad Hanna | 4 | 292 | 17.66 |