Inference of ranking functions for proving temporal properties by abstract interpretation
From MaRDI portal
Publication:681349
DOI10.1016/j.cl.2015.10.001zbMath1379.68101OpenAlexW2217958612MaRDI QIDQ681349
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
Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
Uses Software
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