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

DOI10.1007/s10472-013-9389-zzbMath1329.68172OpenAlexW2053843943MaRDI QIDQ2251128

Jörg Pfähler, Wolfgang Reif, Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst

Publication date: 11 July 2014

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-013-9389-z

zbMATH Keywords

theorem provingconcurrencyspecificationparallel programsinterval temporal logicprogram verificationcompositional reasoninglock-freedomrely-guarantee reasoning

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Distributed Adaptive Systems, Loop verification with invariants and contracts, An application of temporal projection to interleaving concurrency, A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, RGITL: a temporal logic framework for compositional reasoning about interleaved programs, A unifying logic for non-deterministic, parallel and concurrent abstract state machines, Towards a Thread-Local Proof Technique for Starvation Freedom, RGITL, Flashix: modular verification of a concurrent and crash-safe flash file system

Uses Software

• SPIN
• VeriFast
• KIV
• STeP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving linearizability with temporal logic
• Verification of sequential and concurrent programs
• A semantics for concurrent separation logic
• Myths about the mutual exclusion problem
• The Rely-Guarantee method for verifying shared variable concurrent programs
• Deductive verification of real-time systems using STeP
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Interconnections between classes of sequentially compositional temporal formulas
• Prefix and Projection onto State in Duration Calculus
• Formal Verification of a Lock-Free Stack with Hazard Pointers
• A Marriage of Rely/Guarantee and Separation Logic
• Interactive verification of concurrent systems using symbolic execution
• Temporal Logic Verification of Lock-Freedom
• Temporal Verification of Reactive Systems: Response
• Proofs of Networks of Processes
• Abstract State Machines
• Proving that non-blocking algorithms don't block
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Formal Techniques for Networked and Distributed Systems – FORTE 2004