Loop Summarization and Termination Analysis

DOI10.1007/978-3-642-19835-9_9MaRDI QIDQ3000639zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Automated Technology for Verification and Analysis
• Termination analysis of linear loop programs
• TERMINATION ANALYSIS OF LINEAR LOOPS
• Loop Analysis by Quantification over Iterations
• Loop summarization using state and transition invariants
• Symbolic termination analysis of solvable loops
• CONCUR 2005 – Concurrency Theory
• scientific article; zbMATH DE number 4035120
• A Lightweight Approach for Loop Summarization

Cites work

• Loop Summarization Using Abstract Transformers
• Ranking Abstractions
• Ranking Functions for Size-Change Termination II
• Ranking function synthesis for bit-vector relations
• Size-change termination and transition invariants
• Static Analysis
• Summarization for termination: No return!
• The size-change principle for program termination
• Tools and Algorithms for the Construction and Analysis of Systems
• Transition invariants and transition predicate abstraction for program termination
• Variance analyses from invariance analyses
• Verification, Model Checking, and Abstract Interpretation

Cited in

(15)

• Loop summarization using state and transition invariants
• Leaping Loops in the Presence of Abstraction
• TERMINATION ANALYSIS OF LINEAR LOOPS
• Algebraic program analysis
• Loop Summarization Using Abstract Transformers
• Loop summarization with rational vector addition systems
• Ranking functions for linear-constraint loops
• Proving termination through conditional termination
• Conditional Dyck-CFL reachability analysis for complete and efficient library summarization
• Convergence: integrating termination and abort-freedom
• Loop Analysis by Quantification over Iterations
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Extended Nested Dual System Groups, Revisited
• Automated Technology for Verification and Analysis
• A Lightweight Approach for Loop Summarization

Describes a project that uses

Uses Software

• SatAbs
• ARMC

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000639)