Checking Safety Properties Using Induction and a SAT-Solver
The work
| Authors | Mary Sheeran; Satnam Singh; Gunnar Stålmarck |
|---|---|
| Editors | |
| Type | misc |
| Year | 2000 |
| Citekey | sheeran2000checking |
Where it appeared
| Published in | Formal Methods in Computer-Aided Design (FMCAD 2000) |
|---|---|
| Publisher | Springer Science+Business Media |
| Pages | 127--144 |
Identifiers
| DOI | 10.1007/3-540-40922-x_8 |
|---|---|
| OpenAlex | W1495266209 |
Access
| Landing page | https://doi.org/10.1007/3-540-40922-x_8 |
|---|
Empty on purpose
| copy |
Related
| Distinct from | biere1999symbolic |
|---|---|
| Distinct from | bradley2011satbased |
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
We take a fresh look at the problem of how to check safety properties of finite state machines. We are particularly interested in checking safety properties with the help of a SAT-solver. We describe some novel induction-based methods, and show how they are related to more standard fixpoint algorithms for invariance checking. We also present preliminary experimental results in the verification of FPGA cores. This demonstrates the practicality of combining a SAT-solver with induction for safety property checking of hardware in a real design flow.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-09-17 09:43 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{sheeran2000checking,
title = {Checking Safety Properties Using Induction and a SAT-Solver},
author = {Mary Sheeran and Satnam Singh and Gunnar Stålmarck},
year = {2000},
journal = {Formal Methods in Computer-Aided Design (FMCAD 2000)},
publisher = {Springer Science+Business Media},
pages = {127--144},
doi = {10.1007/3-540-40922-x_8},
}
This record lives at https://refs.drheap.org/sheeran2000checking/ and will keep doing so.