The temporal logic of programs
The work
| Authors | Amir Pnueli |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1977 |
| Citekey | pnueli1977temporal |
Where it appeared
| Published in | 18th Annual Symposium on Foundations of Computer Science (sfcs 1977) |
|---|---|
| Pages | 46--57 |
Abstract
A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.
A copy is held
pdf, 1.5 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-22 13:13 UTC |
Cite it as
@inproceedings{pnueli1977temporal,
title = {The temporal logic of programs},
author = {Amir Pnueli},
year = {1977},
booktitle = {18th Annual Symposium on Foundations of Computer Science (sfcs 1977)},
pages = {46--57},
}
This record lives at https://refs.drheap.org/pnueli1977temporal/ and will keep doing so.