Transition predicate abstraction and fair termination

DOI10.1145/1040305.1040317zbMath1369.68152OpenAlexW2042108411MaRDI QIDQ5276141

Andreas Podelski, Andrey Rybalchenko

Publication date: 14 July 2017

Published in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1040305.1040317

zbMATH Keywords

livenessfair terminationsoftware model checkingtransition predicate abstraction

Mathematics Subject Classification ID

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

Related Items

Predicate Abstraction for Program Verification ⋮ A type-based complexity analysis of object oriented programs ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Combining Predicate Abstraction with Fixpoint Approximations ⋮ Transition Invariants and Transition Predicate Abstraction for Program Termination ⋮ Model checking duration calculus: a practical approach ⋮ Inference of ranking functions for proving temporal properties by abstract interpretation ⋮ Explicit Fair Scheduling for Dynamic Control ⋮ Partial predicate abstraction and counter-example guided refinement ⋮ Temporal prophecy for proving temporal properties of infinite-state systems ⋮ Automated formal analysis and verification: an overview ⋮ Automatic Verification of Combined Specifications: An Overview