Proving liveness of parameterized programs

DOI10.1145/2933575.2935310MaRDI QIDQ4635874zbMATH OpenOpenAlexFDO

Authors Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.02350

Mathematics Subject Classification ID

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

Abstract: Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold regardless of the number of threads that are active in the program.

Recommendations

• Proving Liveness by Backwards Reachability
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Proof spaces for unbounded parallelism
• scientific article; zbMATH DE number 1670786
• A shared-variable concurrency analysis of multi-threaded object-oriented programs

Cited in

(9)

• Verifying the correctness of distributed systems via mergeable parallelism
• Sound verification procedures for temporal properties of infinite-state systems
• Reachability in parameterized systems: all flavors of threshold automata
• Domains for Higher-Order Games
• Proving Liveness by Backwards Reachability
• Parity to safety in polynomial time for pushdown and collapsible pushdown systems
• Temporal prophecy for proving temporal properties of infinite-state systems
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Commutativity for concurrent program termination proofs

This page was built for publication: Proving liveness of parameterized programs

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