An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)
The work
| Authors | Moshe Y. Vardi; Pierre Wolper |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1986 |
| Citekey | vardi1986automatatheoretic |
Where it appeared
| Published in | Proceedings of the First Annual Symposium on Logic in Computer Science |
|---|---|
| Pages | 332--344 |
Access
| Free full text | https://orbi.uliege.be/bitstream/2268/116609/1/lics86.pdf |
|---|
Related
| Distinct from | bouzafour2018modelchecking |
|---|---|
| Distinct from | bryant1986graphbased |
| Distinct from | burch1992symbolic |
| Distinct from | clarke1981design |
| Distinct from | clarke1986automatic |
| Distinct from | halpern2001unusual |
| Distinct from | holzmann1997model |
| Distinct from | vardi1994reasoning |
Abstract
We describe an automata-theoretic approach to automatic verification of concurrent finite-state programs by model checking. The basic idea underlying this approach is that for any temporal formula we can construct an automaton that accepts precisely the computations that satisfy the formula. The model-checking algorithm that results from this approach is much simpler and cleaner than tableau-based algorithms. We use this approach to extend model-checking to probabilistic concurrent finite-state programs.
A copy is held
pdf, 836.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | import via bibtex |
|---|---|
| Added | 2026-08-23 00:00 UTC |
| Approved by | a person 2026-10-05 21:07 UTC |
Filed under
Cite it as
@inproceedings{vardi1986automatatheoretic,
title = {An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)},
author = {Moshe Y. Vardi and Pierre Wolper},
year = {1986},
booktitle = {Proceedings of the First Annual Symposium on Logic in Computer Science},
pages = {332--344},
}
This record lives at https://refs.drheap.org/vardi1986automatatheoretic/ and will keep doing so.