Termination Analysis with Calling Context Graphs

DOI10.1007/11817963_36MaRDI QIDQ5756741zbMATH OpenOpenAlexFDO

Authors Panagiotis Manolios, Daron Vroon

Publication date 5 September 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11817963_36

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Recommendations

• Interactive Termination Proofs Using Termination Cores
• Termination analysis for partial functions
• The size-change principle for program termination
• Termination analysis for functional programs
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages

Cited in

(18)

• All-Termination(T)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Adapting functional programs to higher order logic
• Summarization for termination: No return!
• Formal verification of termination criteria for first-order recursive functions
• Run-time complexity bounds using squeezers
• Termination Analysis by Dependency Pairs and Inductive Theorem Proving
• Integrating testing and interactive theorem proving
• Proving termination by dependency pairs and inductive theorem proving
• A SAT-Based Approach to Size Change Termination with Global Ranking Functions
• Termination analysis for partial functions
• Termination analysis and call graph construction for higher-order functional programs
• scientific article; zbMATH DE number 7453196 (Why is no real title available?)
• Asymptotically precise ranking functions for deterministic size-change systems
• ACL2s: ``the ACL2 sedan
• The ACL2 Sedan theorem proving system
• Formalization of the computational theory of a Turing complete functional language model
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages

Describes a project that uses

Uses Software

• AProVE
• ACL2

This page was built for publication: Termination Analysis with Calling Context Graphs

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