Summarization for termination: No return!

DOI10.1007/s10703-009-0087-8zbMath1185.68412OpenAlexW2149745672MaRDI QIDQ845247

Andrey Rybalchenko, Andreas Podelski, Byron Cook

Publication date: 5 February 2010

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-009-0087-8

zbMATH Keywords

TerminationModel checkingKeywords: Program verificationRecursionSummarization

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (3)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Loop Summarization and Termination Analysis ⋮ Loop summarization using state and transition invariants

Uses Software

• SPIN
• ARMC
• Bebop

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Weighted pushdown systems and their application to interprocedural dataflow analysis
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Interprocedural analysis of asynchronous programs
• Proving non-termination
• Summarizing procedures in concurrent programs
• Visibly pushdown languages
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Efficient algorithms for pre* and post* on interprocedural parallel flow graphs
• The size-change principle for program termination
• Tools and Algorithms for the Construction and Analysis of Systems
• Programming Languages and Systems
• A fixpoint calculus for local and global program flows
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• Program Analysis Using Weighted Pushdown Systems
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Termination Analysis with Calling Context Graphs
• Improving Pushdown System Model Checking
• Static Analysis

This page was built for publication: Summarization for termination: No return!