Summarization for termination: No return!

DOI10.1007/S10703-009-0087-8zbMATH Open1185.68412OpenAlexW2149745672MaRDI QIDQ845247FDOQ845247

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

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

zbMATH Keywords

Model checkingKeywords: Program verificationRecursionSummarizationTermination

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

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

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)