SAT-Based Model Checking without Unrolling
The work
| Authors | Aaron R. Bradley |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2011 |
| Citekey | bradley2011satbased |
Where it appeared
| Published in | Verification, Model Checking, and Abstract Interpretation (VMCAI) |
|---|---|
| Publisher | Springer Berlin Heidelberg |
| Series | Lecture Notes in Computer Science |
| Pages | 70--87 |
Identifiers
| DOI | 10.1007/978-3-642-18275-4_7 |
|---|---|
| ISSN | 0302-9743 |
| ISBN | 978-3-642-18274-7 |
Access
| Landing page | https://doi.org/10.1007/978-3-642-18275-4_7 |
|---|
Related
| Distinct from | biere1999symbolic |
|---|---|
| Distinct from | bryant1986graphbased |
| Distinct from | bryant2018binary |
| Distinct from | burch1992symbolic |
| Distinct from | cabodi2016hardware |
| Distinct from | een2011efficient |
| Distinct from | lewis2026finding |
| Distinct from | mishchenko2005fraigs |
| Distinct from | seufert2026certified |
From crossref.
Abstract
A new form of SAT-based symbolic model checking is described. Instead of unrolling the transition relation, it incrementally generates clauses that are inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful tool for generalizing the unreachability of given error states: it can refine away many states at once, and it is effective at focusing the proof search on aspects of the transition system relevant to the property. Furthermore, the incremental structure of the algorithm lends itself to a parallel implementation.
A copy is held
pdf, 228.1 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-16 08:04 UTC |
| Approved by | a person 2026-10-02 09:57 UTC |
Filed under
Cite it as
@inproceedings{bradley2011satbased,
title = {SAT-Based Model Checking without Unrolling},
author = {Aaron R. Bradley},
year = {2011},
booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
pages = {70--87},
isbn = {978-3-642-18274-7},
issn = {0302-9743},
doi = {10.1007/978-3-642-18275-4_7},
}
This record lives at https://refs.drheap.org/bradley2011satbased/ and will keep doing so.