Inference of ranking functions for proving temporal properties by abstract interpretation

DOI10.1016/j.cl.2015.10.001zbMath1379.68101OpenAlexW2217958612MaRDI QIDQ681349

Antoine Miné, Caterina Urban

Publication date: 30 January 2018

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://hal.sorbonne-universite.fr/hal-01312239/file/article-urban-mine-comlan2015.pdf

zbMATH Keywords

livenessstatic analysisterminationabstract interpretationranking functionstemporal properties

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Temporal prophecy for proving temporal properties of infinite-state systems

Uses Software

• Apron

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The octagon abstract domain
• Conflict-driven conditional termination
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Verification of concurrent programs: The automata-theoretic framework
• Policy Iteration-Based Conditional Termination and Ranking Functions
• An abstract interpretation framework for termination
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Variance analyses from invariance analyses
• Proving that programs eventually do something good
• Counterexample-guided abstraction refinement for symbolic model checking
• Proving Conditional Termination
• Proving the Correctness of Multiprocess Programs
• Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations
• Transition predicate abstraction and fair termination
• Algebraic Methodology and Software Technology
• An Abstract Domain to Infer Ordinal-Valued Ranking Functions

This page was built for publication: Inference of ranking functions for proving temporal properties by abstract interpretation