RGITL: a temporal logic framework for compositional reasoning about interleaved programs (Q2251128)

This paper describes a rich temporal logic, called RGITL, for the specification and verification of parallel programs. The logic is based on Interval Temporal Logic in the sense that it allows assertions to be made about finite and infinite sequences of program runs, including the concatenation thereof. Programs to be verified are specified using a WHILE-like programming language with parallel composition. Formulas and programs are mixed together to form the specification language RGITL, i.e.\ the verification framework is not based on an explicit translation of programs into transition systems for instance. Instead, the program dynamics are modelled using symbolic execution which amounts to syntactic transformations of program terms that reveals the next step of what the program does. The paper describes how RGITL can be used in theorem proving, i.e.\ it gives proof rules that are tailored towards particular goals in terms of specific properties to be verified, namely fairness, lock-freedom and rely-guarantee properties. It describes a general induction principle for proving such properties in the presence of interleaving programs. Particular focus is put onto compositional reasoning, i.e.\ the decomposition of properties with proof rules into parts that need to hold on parallel components separately. The framework is implemented and available in the theorem prover KIV.