×

zbMATH — the first resource for mathematics

On temporal program verification rules. (English) Zbl 0563.68007
This paper suggests a slight extension of the usual temporal logical framework for the description and verification of programs. With this extension it is possible to give elegant and transparent formulations of proof rules for formulas expressing program properties. Besides the transcription of well-known rules the paper particularly deals with formulas containing the recently introduced atnext operator.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: EuDML
References:
[1] 1. F. KRÖGER, Some new aspects of the temporal logic of concurrent programs, Technical University of Munich, Institute of Informatics, Report I8311 (1983).
[2] 2. F. KRÖGER, A generalized nexttime operator, JCSS 29, 80-98 (1984). Zbl0551.68032 MR761053 · Zbl 0551.68032
[3] 3. Z. MANNA and A. PNUELI, Verification of concurrent programs : The temporal framework, in : The correctness problem in computer science (R. S. Boyer and J. S. Moore, eds.), International Lecture Series in Computer Science, Academic Press, London 1981.
[4] 4. Z. MANNA and A. PNUELI, Verification of concurrent programs: Temporal proof principles, in : Logics of programs, Proc. 1981, Springer LNCS 131, 200-252 (1981). Zbl0481.68019 MR663759 · Zbl 0481.68019
[5] 5. Z. MANNA and A. PNUELI, Proving precedence properties : The temporal way, in : Proc. 10th ICALP, Springer LNCS 154, 491-512 (1983). Zbl0528.68008 MR727678 · Zbl 0528.68008
[6] 6. G. L. PETERSON, Myths about the mutual exclusion problem, Information Processing Letters 12, 115-116 (1981). Zbl0474.68031 · Zbl 0474.68031
[7] 7. A. PNUELI, The temporal semantics of concurrent programs, Theor. Comp. Science 13, 45-60 (1981). Zbl0441.68010 MR593863 · Zbl 0441.68010
[8] 8. H. SCHLINGLOFF, Beweistheoretische Untersuchungen zur temporalen Logik, Diploma thesis, Technical University of Munich, Institute of Informatics (1983).
[9] 9. P. WOLPER, Temporal logic can be more expressive, Proc. 22nd Symp. on Found. of Comp. Sci., Nashville, TN, 340-348 (1981).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.