Model checking and abstraction
The work
| Authors | Edmund M. Clarke; Orna Grümberg; David E. Long |
|---|---|
| Editors | |
| Type | misc |
| Year | 1992 |
| Citekey | clarke1992model |
Where it appeared
| Published in | ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) |
|---|---|
| Pages | 343--354 |
Identifiers
| DOI | 10.1145/143165.143235 |
|---|---|
| OpenAlex | W2114092850 |
Access
| Landing page | https://doi.org/10.1145/143165.143235 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/143165.143235 |
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. The basis of this method is a way of constructing 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 pipelined ALU circuit with over 101300 states.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-23 21:16 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{clarke1992model,
title = {Model checking and abstraction},
author = {Edmund M. Clarke and Orna Grümberg and David E. Long},
year = {1992},
journal = {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
pages = {343--354},
doi = {10.1145/143165.143235},
}
This record lives at https://refs.drheap.org/clarke1992model/ and will keep doing so.