Efficient implementation of property directed reachability
The work
| Authors | Niklas Eén; Alan Mishchenko; Robert K. Brayton |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2011 |
| Citekey | een2011efficient |
Where it appeared
| Published in | Formal Methods in Computer-Aided Design (FMCAD) |
|---|---|
| Publisher | FMCAD Inc. |
| Pages | 125--134 |
Identifiers
| DOI | 10.5555/2157654.2157675 |
|---|---|
| OpenAlex | W2118791871 |
Access
| Landing page | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.7486 |
|---|---|
| Free full text | https://people.eecs.berkeley.edu/~alanmi/publications/2011/fmcad11_pdr.pdf |
Related
| Distinct from | andrici2019verifying |
|---|---|
| Distinct from | bradley2011satbased |
| Distinct from | chakraborty2015wordlevel |
| Distinct from | mishchenko2005fraigs |
| Distinct from | nukala2024translating |
| Distinct from | seufert2026certified |
| Distinct from | slobodova2011flexible |
| Distinct from | tan2026secic3 |
| Distinct from | yu2025fraigbmc |
| Distinct from | zhang2025fastlec |
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
Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.
A copy is held
pdf, 245.4 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 19:24 UTC |
| Approved by | a person 2026-09-16 21:23 UTC |
Filed under
Cite it as
@inproceedings{een2011efficient,
title = {Efficient implementation of property directed reachability},
author = {Niklas Eén and Alan Mishchenko and Robert K. Brayton},
year = {2011},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
publisher = {FMCAD Inc.},
pages = {125--134},
doi = {10.5555/2157654.2157675},
}
This record lives at https://refs.drheap.org/een2011efficient/ and will keep doing so.