Convergence: integrating termination and abort-freedom

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

zbMATH Keywords

convergenceterminationinvariant relationsiterative programsabort-freedom

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Toward a theory of program repair

Uses Software

• NQTHM
• CalcCheck
• ASTREE
• Looper

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