Convergence: integrating termination and abort-freedom
From MaRDI portal
Publication:1647960
DOI10.1016/j.jlamp.2018.02.001zbMath1395.68091OpenAlexW2790776996MaRDI QIDQ1647960
Wided Ghardallou, Jules Desharnais, Nafi Diallo, Ali Milli
Publication date: 27 June 2018
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2018.02.001
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A versatile concept for the analysis of loops
- Reflexive transitive invariant relations: A basis for computing loop functions
- Magic-sets for localised analysis of Java bytecode
- Strongest invariant functions: Their use in the systematic analysis of while statements
- Mathematics for reasoning about loop functions
- Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
- Invariant functions and invariant relations: an alternative to invariant assertions
- Rigorous software development. An introduction to program verification.
- Proving pointer programs in higher-order logic
- A Modular Static Analysis Approach to Affine Loop Invariants Detection
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Loop Summarization and Termination Analysis
- Proving non-termination
- Lifting abstract interpreters to quantified logical domains
- Bottom-Up Shape Analysis
- Proving Conditional Termination
- Relational Methods in Computer Science
- Computer Aided Verification
- Ramsey vs. Lexicographic Termination Proving
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Ranking Abstractions
- Non-termination Checking for Imperative Programs
- An axiomatic basis for computer programming
- Computer Aided Verification
- Automata, Languages and Programming
- Static Analysis
- CONCUR 2005 – Concurrency Theory
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation