Proving Liveness by Backwards Reachability

DOI10.1007/11817949_7MaRDI QIDQ5756597zbMATH OpenOpenAlexFDO

Authors Ahmed Rezine, Mayank Saksena, Parosh A. Abdulla, Bengt Jonsson

Publication date 4 September 2007

Published in CONCUR 2006 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11817949_7

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Proving liveness of parameterized programs
• Frontiers of Combining Systems
• Publication:4945222
• Liveness Reasoning with Isabelle/HOL
• scientific article; zbMATH DE number 177840
• scientific article; zbMATH DE number 177518

Cited in

(8)

• Temporal prophecy for proving temporal properties of infinite-state systems
• Parameterized verification of leader/follower systems via first-order temporal logic
• Proving non-termination
• Temporal Verification of Fault-Tolerant Protocols
• Proving liveness of parameterized programs
• Verifying liveness for asynchronous programs
• Proving liveness of fair transition systems
• A new approach for showing termination of parameterized transition systems

This page was built for publication: Proving Liveness by Backwards Reachability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756597)