Transition predicate abstraction and fair termination

DOI10.1145/1040305.1040317MaRDI QIDQ5276141zbMATH OpenOpenAlexFDO

Authors 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

fair terminationlivenesssoftware model checkingtransition predicate abstraction

Mathematics Subject Classification ID

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

Recommendations

• Predicate abstraction for program verification
• Automated Technology for Verification and Analysis
• A symbolic approach to predicate abstraction.
• Transition invariants and transition predicate abstraction for program termination
• Formal Techniques for Networked and Distributed Systems - FORTE 2005

Cited in

(16)

• A type-based complexity analysis of object oriented programs
• Temporal prophecy for proving temporal properties of infinite-state systems
• Partial predicate abstraction and counter-example guided refinement
• Automated formal analysis and verification: an overview
• Automatic verification of combined specifications: an overview
• Transition invariants and transition predicate abstraction for program termination
• Predicate abstraction for program verification
• Combining Predicate Abstraction with Fixpoint Approximations
• Explicit fair scheduling for dynamic control
• Model Checking Software
• Progress measures and stack assertions for fair termination
• First order Büchi automata and their application to verification of LTL specifications
• 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
• Deciding Boolean algebra with Presburger arithmetic
• Model checking duration calculus: a practical approach

This page was built for publication: Transition predicate abstraction and fair termination

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