Summarization for termination: No return!

DOI10.1007/S10703-009-0087-8MaRDI QIDQ845247zbMATH OpenOpenAlexFDO

Authors Byron Cook, Andreas Podelski, Andrey Rybalchenko

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

Model checkingKeywords: Program verificationRecursionSummarizationTermination

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 3930339
• Termination by completion
• Uncurrying for Termination
• Simple termination revisited
• Topics in termination
• Left termination turned into termination
• Simple termination is difficult
• Simple termination is difficult
• Alternation for termination

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• scientific article; zbMATH DE number 1903370 (Why is no real title available?)
• A fixpoint calculus for local and global program flows
• Efficient algorithms for pre* and post* on interprocedural parallel flow graphs
• Improving Pushdown System Model Checking
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Interprocedural analysis of asynchronous programs
• Program Analysis Using Weighted Pushdown Systems
• Programming Languages and Systems
• Proving non-termination
• Static Analysis
• Static Analysis
• Summarizing procedures in concurrent programs
• Termination Analysis with Calling Context Graphs
• 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
• Verification, Model Checking, and Abstract Interpretation
• Visibly pushdown languages
• Weighted pushdown systems and their application to interprocedural dataflow analysis

Cited in

(5)

• Loop summarization using state and transition invariants
• Loop Summarization and Termination Analysis
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Programming Languages and Systems
• Underapproximation of procedure summaries for integer programs

Describes a project that uses

Uses Software

• SPIN
• ARMC
• Bebop

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

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