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 selfcontained presentation of the temporal logic RelyGuarantee Interval Temporal Logic (RGITL). The logic is based on interval temporal logic (ITL) and higherorder 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 relyguarantee (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 lockfreedom. 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 lockfree algorithms. 
Homepage: 
http://link.springer.com/article/10.1007%2Fs104720139389z

Keywords: 
specification;
verification;
theorem proving;
interval temporal logic

Related Software: 
SPIN;
KIV;
Dafny;
GNATprove;
Isabelle/HOL;
CIRC;
CPAchecker;
HolBA;
SeaHorn;
Leon;
Rodin;
Lineup;
Z;
STeP;
VeriFast

Cited in: 
8 Documents
