ISSE

Search

RGITL: A Temporal Logic Framework for Compositional Reasoning about Interleaved Programs

G. Schellhorn, B. Tofan, G. Ernst, J. Pfähler, and W. Reif

RGITL: A Temporal Logic Framework for Compositional Reasoning about Interleaved Programs

This paper gives a self-contained presentation of the temporal logic Rely-Guarantee Interval Temporal Logic (RGITL). The logic is based on inter- val temporal logic and higher-order logic. It extends ITL with explicit interleaved programs and recursive procedures. Deduction is based on the principles of sym- bolic execution and induction, known from the verification of sequential programs, which are transferred to a concurrent setting with full temporal logic. We include an interleaving operator with compositional semantics. As a consequence, the cal- culus permits to prove decomposition theorems, which reduce reasoning about an interleaved program to reasoning about individual threads. A central instance of such theorems are rely-guarantee (RG) rules, which decompose global safety prop- erties, and we show how the correctness of such rules can be formally derived in the calculus. Decomposition theorems for other global properties are also deriv- able, as we show for the important progress property of lock-freedom. RGITL is implemented in the interactive verification environment KIV. It has been used to mechanize various proofs for concurrent algorithms, mainly in the area of linearizable and lock-free algorithms.

Springer link , link to draft version
published 2014 Annals of Mathematics and Artificial Intelligence (AMAI) Journal, vol. 71, issue 1-3, pp. 131-174

Publisher: Springer