Proving that programs eventually do something good

DOI10.1145/1190216.1190257zbMath1295.68083OpenAlexW3160870209MaRDI QIDQ3189807

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

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

livenessformal verificationterminationsoftware model checking

Mathematics Subject Classification ID

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

Related Items (9)

Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Temporal property verification as a program analysis task ⋮ Liveness-Preserving Atomicity Abstraction ⋮ Inference of ranking functions for proving temporal properties by abstract interpretation ⋮ Proving Stabilization of Biological Systems ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof ⋮ Proving the Correctness of the Implementation of a Control-Command Algorithm ⋮ Operating system verification---an overview ⋮ Streett Automata Model Checking of Higher-Order Recursion Schemes

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