Model checking and abstraction
The work
| Authors | Edmund M. Clarke; Orna Grümberg; David E. Long |
|---|---|
| Editors | |
| Type | article |
| Year | 1994 |
| Citekey | clarke1994model |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 16 |
| Issue | 5 |
| Pages | 1512--1542 |
Identifiers
| DOI | 10.1145/186025.186051 |
|---|---|
| OpenAlex | W2080593426 |
Access
| Landing page | https://doi.org/10.1145/186025.186051 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/186025.186051 |
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 describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10 1300 states.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 01:38 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{clarke1994model,
title = {Model checking and abstraction},
author = {Edmund M. Clarke and Orna Grümberg and David E. Long},
year = {1994},
journal = {ACM Transactions on Programming Languages and Systems},
publisher = {Association for Computing Machinery},
volume = {16},
number = {5},
pages = {1512--1542},
doi = {10.1145/186025.186051},
}
This record lives at https://refs.drheap.org/clarke1994model/ and will keep doing so.