The temporal logic of programs
- 1 September 1977
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 46-57
- https://doi.org/10.1109/sfcs.1977.32
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.Keywords
This publication has 13 references indexed in Scilit:
- Is “sometime” sometimes better than “always”?Communications of the ACM, 1978
- A proof method for cyclic programsActa Informatica, 1978
- Computability and completeness in logics of programs (Preliminary Report)Published by Association for Computing Machinery (ACM) ,1977
- Propositional modal logic of programsPublished by Association for Computing Machinery (ACM) ,1977
- Formal verification of parallel programsCommunications of the ACM, 1976
- Verifying properties of parallel programsCommunications of the ACM, 1976
- Axiomatic approach to total correctness of programsActa Informatica, 1974
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967
- Semantical Analysis of Modal Logic I Normal Modal Propositional CalculiMathematical Logic Quarterly, 1963