The temporal logic of programs
作者： Amir Pnueli
DOI: 10.1109/SFCS.1977.32
关键词: Deductive reasoning 、 Temporal logic of actions 、 Property Specification Language 、 Automated reasoning 、 Programming language 、 Temporal logic 、 Computation tree logic 、 Computer science 、 Theoretical computer science 、 Interval temporal logic 、 Linear temporal logic
摘要: A unified approach to program verification is suggested, which applies both sequential and parallel programs. The main proof method suggested that of temporal reasoning in the time dependence events basic concept. Two formal systems are presented for providing a basis reasoning. One forms formalization intermittent assertions, while other an adaptation tense logic system Kb, particularly suitable about concurrent
ieeecomputersociety.org
acm.org 参考文章(15)
Edward A. Ashcroft, William W. Wadge, Intermittent Assertion Proofs in Lucid. ifip congress. pp. 723- 726 ,(1977)
Susan Owicki, David Gries, An axiomatic proof technique for parallel programs I Acta Informatica. ,vol. 6, pp. 319- 340 ,(1976) , 10.1007/BF00268134
Susan Owicki, David Gries, Verifying properties of parallel programs Communications of the ACM. ,vol. 19, pp. 279- 285 ,(1976) , 10.1145/360051.360224
D. Harel, A. R. Meyer, V. R. Pratt, Computability and completeness in logics of programs (Preliminary Report) symposium on the theory of computing. pp. 261- 268 ,(1977) , 10.1145/800105.803416
Michael J. Fischer, Richard E. Ladner, Propositional modal logic of programs symposium on the theory of computing. pp. 286- 294 ,(1977) , 10.1145/800105.803418
Robert M. Keller, Formal verification of parallel programs Communications of The ACM. ,vol. 19, pp. 371- 384 ,(1976) , 10.1145/360248.360251
Zohar Manna, Richard Waldinger, Is “sometime” sometimes better than “always”? Communications of the ACM. ,vol. 21, pp. 159- 172 ,(1978) , 10.1145/359340.359353
Zohar Manna, Amir Pnueli, Axiomatic approach to total correctness of programs Acta Informatica. ,vol. 3, pp. 243- 263 ,(1973) , 10.1007/BF00288637
Nissim Francez, Amir Pnueli, A proof method for cyclic programs Acta Informatica. ,vol. 9, pp. 133- 157 ,(1978) , 10.1007/BF00289074
Saul A. Kripke, Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. ,vol. 9, pp. 67- 96 ,(1963) , 10.1002/MALQ.19630090502