RGITL swMATH ID: 13917 Software Authors: Schellhorn, Gerhard; Tofan, Bogdan; Ernst, Gidon; Pf"ahler, Jörg; Reif, Wolfgang Description: 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 interval temporal logic (ITL) and higher-order logic. It extends ITL with explicit interleaved programs and recursive procedures. Deduction is based on the principles of symbolic execution and induction, known from the verification of sequential programs, which are transferred to a concurrent setting with temporal logic. We include an interleaving operator with compositional semantics. As a consequence, the calculus permits proving 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 properties. We show how the correctness of such rules can be formally derived in the calculus. Decomposition theorems for other global properties are also derivable, 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 of concurrent algorithms, mainly in the area oflinearizable and lock-free algorithms. Homepage: http://link.springer.com/article/10.1007%2Fs10472-013-9389-z Keywords: specification; verification; theorem proving; interval temporal logic Related Software: SPIN; KIV; Dafny; GNATprove; Isabelle/HOL; CIRC; CPAchecker; HolBA; SeaHorn; Leon; Rodin; Line-up; Z; STeP; VeriFast Cited in: 8 Documents Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Zbl 1329.68172Schellhorn, Gerhard; Tofan, Bogdan; Ernst, Gidon; Pfähler, Jörg; Reif, Wolfgang 2014 all top 5 Cited by 16 Authors 4 Schellhorn, Gerhard 2 Ernst, Gidon 2 Ferrarotti, Flavio Antonio 2 Reif, Wolfgang 2 Schewe, Klaus-Dieter 2 Tec, Loredana 2 Wang, Qing 2 Wehrheim, Heike 1 Bitterlich, Martin 1 Bodenmüller, Stefan 1 Derrick, John 1 Guelev, Dimitar P. 1 Moszkowski, Ben C. 1 Pfähler, Jörg 1 Tofan, Bogdan 1 Travkin, Oleg Cited in 3 Serials 2 Annals of Mathematics and Artificial Intelligence 1 Formal Aspects of Computing 1 ACM Transactions on Computational Logic Cited in 2 Fields 8 Computer science (68-XX) 4 Mathematical logic and foundations (03-XX) Citations by Year