Loop Summarization and Termination Analysis

DOI10.1007/978-3-642-19835-9_9zbMath1315.68106OpenAlexW1500350535MaRDI QIDQ3000639

Daniel Kroening, Christoph M. Wintersteiger, Natasha Sharygina, Aliaksei Tsitovich

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_9

Mathematics Subject Classification ID

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

Related Items (6)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Algebraic program analysis ⋮ Convergence: integrating termination and abort-freedom ⋮ Proving Termination Through Conditional Termination ⋮ Extended Nested Dual System Groups, Revisited ⋮ Ranking Functions for Linear-Constraint Loops

Uses Software

• ARMC
• SatAbs

Cites Work

• Summarization for termination: No return!
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Variance analyses from invariance analyses
• Loop Summarization Using Abstract Transformers
• Ranking Function Synthesis for Bit-Vector Relations
• Ranking Functions for Size-Change Termination II
• Size-Change Termination and Transition Invariants
• The size-change principle for program termination
• Ranking Abstractions
• Tools and Algorithms for the Construction and Analysis of Systems
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Loop Summarization and Termination Analysis