zbMATH — the first resource for mathematics

A sequent calculus for first-order dynamic logic with trace modalities. (English) Zbl 0988.03051
Goré, Rajeev (ed.) et al., Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2083, 626-641 (2001).
Summary: The modalities of dynamic logic refer to the final state of a program execution and allow to specify programs with pre- and post-conditions. In this paper, we extend dynamic logic with additional trace modalities “throughout” and “at least once”, which refer to all the states a program reaches. They allow one to specify and verify invariants and safety constraints that have to be valid throughout the execution of a program. We give a sound and (relatively) complete sequent calculus for this extended dynamic logic.
For the entire collection see [Zbl 0968.00052].

03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link