Proving that programs eventually do something good

DOI10.1145/1190216.1190257MaRDI QIDQ3189807zbMATH OpenOpenAlexFDO

Authors Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi

Publication date 12 September 2014

Published in Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL http://edoc.mpg.de/356677

zbMATH Keywords

formal verificationlivenesssoftware model checkingtermination

Mathematics Subject Classification ID

Distributed systems (68M14) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Proving guarantee and recurrence temporal properties by abstract interpretation
• Inference of ranking functions for proving temporal properties by abstract interpretation
• Proof Pearl: The Termination Analysis of Terminator
• Syntax directed analysis of liveness properties of while programs
• Symbolic liveness analysis of real-world software

Cited in

(13)

• Operating system verification---an overview
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Temporal property verification as a program analysis task
• Liveness-Preserving Atomicity Abstraction
• Proving stabilization of biological systems
• Proving the Correctness of the Implementation of a Control-Command Algorithm
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Proving guarantee and recurrence temporal properties by abstract interpretation
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Multiphase-linear ranking functions and their relation to recurrent sets
• An overview of the HFL model checking project
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Inference of ranking functions for proving temporal properties by abstract interpretation

This page was built for publication: Proving that programs eventually do something good

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