Symbolic Model Checking without BDDs
The work
| Authors | Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Yunshan Zhu |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1999 |
| Citekey | biere1999symbolic |
Where it appeared
| Published in | Tools and Algorithms for the Construction and Analysis of Systems (TACAS) |
|---|---|
| Publisher | Springer Science+Business Media |
| Series | Lecture Notes in Computer Science |
| Pages | 193--207 |
Identifiers
| DOI | 10.1007/3-540-49059-0_14 |
|---|---|
| OpenAlex | W1787074469 |
Access
| Landing page | https://doi.org/10.1007/3-540-49059-0_14 |
|---|
Related
| Distinct from | bradley2011satbased |
|---|---|
| Distinct from | bryant1986graphbased |
| Distinct from | bryant2018binary |
| Distinct from | burch1992symbolic |
| Distinct from | cabodi2016hardware |
| Distinct from | davis2013verified |
| Distinct from | ferres2023electrical |
| Distinct from | lee2026formal |
| Distinct from | manjrekar2025automating |
| Distinct from | melham1990formalizing |
| Distinct from | peng2015extending |
| Distinct from | plassanconclusive |
| Distinct from | seger1995formal |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
Symbolic Model Checking [3, 14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stålmarck’s Method [16] or the Davis & Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability. We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented.
A copy is held
pdf, 123.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-09-16 07:35 UTC |
| Approved by | a person 2026-10-02 10:00 UTC |
Filed under
Cite it as
@inproceedings{biere1999symbolic,
title = {Symbolic Model Checking without BDDs},
author = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan Zhu},
year = {1999},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
publisher = {Springer Science+Business Media},
series = {Lecture Notes in Computer Science},
pages = {193--207},
doi = {10.1007/3-540-49059-0_14},
}
This record lives at https://refs.drheap.org/biere1999symbolic/ and will keep doing so.