Apt, Krzysztof R.; Delporte-Gallet, Carole Syntax directed analysis of liveness properties of while programs. (English) Zbl 0591.68016 Inf. Control 68, 223-253 (1986). Summary: A syntax directed proof system which allows to prove liveness properties of while-programs is introduced. The proof system is proved to be arithmetically sound and complete in the sense of D. Harel [First- order dynamic logic, Berlin (1979; Zbl 0403.03024)]. The results of the paper generalize a corresponding result A. Pnueli [Proc. 18th Sympos. FOCS, IEEE, Providence, R. I., 46-57 (1977)] proves for unstructured programs. The proof system decomposes into two parts. The first part allows to prove simple safety properties. These properties are used as axioms in the second proof system which deals with liveness properties. The completeness proof is constructive and provides a heuristic for proving specific liveness properties. Cited in 2 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68N01 General topics in the theory of software Keywords:syntax directed proof system; liveness properties; while-programs Citations:Zbl 0403.03024 PDFBibTeX XMLCite \textit{K. R. Apt} and \textit{C. Delporte-Gallet}, Inf. Control 68, 223--253 (1986; Zbl 0591.68016) Full Text: DOI