The size-change principle for program termination
From MaRDI portal
Publication:5178875
DOI10.1145/360204.360210zbMath1323.68216OpenAlexW1993129359WikidataQ57483905 ScholiaQ57483905MaRDI QIDQ5178875
Neil D. Jones, Chin Soon Lee, Amir M. Ben-Amram
Publication date: 17 March 2015
Published in: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/360204.360210
Formal languages and automata (68Q45) Functional programming and lambda calculus (68N18) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (61)
\textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programs ⋮ Ramsey-Based Inclusion Checking for Visibly Pushdown Automata ⋮ A combination framework for complexity ⋮ On the Termination of Integer Loops ⋮ On proving \(C_E\)-termination of rewriting by size-change termination ⋮ Size-Change Termination and Satisfiability for Linear-Time Temporal Logics ⋮ Predicate Abstraction for Program Verification ⋮ Summarization for termination: No return! ⋮ Verifying termination and reduction properties about higher-order logic programs ⋮ Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems ⋮ Asynchronous unfold/fold transformation for fixpoint logic ⋮ Mechanizing and improving dependency pairs ⋮ Termination of linear programs with nonlinear constraints ⋮ Size-based termination of higher-order rewriting ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Parameterized recursive refinement types for automated program verification ⋮ Distributing and parallelizing non-canonical loops ⋮ Formal verification of termination criteria for first-order recursive functions ⋮ Abstract cyclic proofs ⋮ Complete and tractable machine-independent characterizations of second-order polytime ⋮ Fast offline partial evaluation of logic programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Strength of the SCT Criterion ⋮ The Computability Path Ordering: The End of a Quest ⋮ Proving termination of nonlinear command sequences ⋮ Verification and code generation for invariant diagrams in Isabelle ⋮ Loop Summarization and Termination Analysis ⋮ Enhancing dependency pair method using strong computability in simply-typed term rewriting ⋮ Run-time complexity bounds using squeezers ⋮ A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees ⋮ An intuitionistic version of Ramsey's theorem and its use in program termination ⋮ Loop summarization using state and transition invariants ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys ⋮ A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs ⋮ Büchi Complementation and Size-Change Termination ⋮ All-Termination(T) ⋮ A SAT-Based Approach to Size Change Termination with Global Ranking Functions ⋮ Decision Procedures for Automating Termination Proofs ⋮ A complexity tradeoff in ranking-function termination proofs ⋮ Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic Programs ⋮ Unnamed Item ⋮ A novel learning algorithm for Büchi automata based on family of DFAs and classification trees ⋮ Advanced Ramsey-Based Büchi Automata Inclusion Testing ⋮ Automata-Based Termination Proofs ⋮ RAMSEY’S THEOREM FOR PAIRS ANDKCOLORS AS A SUB-CLASSICAL PRINCIPLE OF ARITHMETIC ⋮ Adapting functional programs to higher order logic ⋮ Ranking Functions for Linear-Constraint Loops ⋮ Unnamed Item ⋮ Proving Termination with (Boolean) Satisfaction ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ The size-change principle and dependency pairs for termination of term rewriting ⋮ Formalization of the computational theory of a Turing complete functional language model ⋮ Type-level Computation Using Narrowing in Ωmega ⋮ ACL2s: “The ACL2 Sedan” ⋮ A second-order formulation of non-termination
This page was built for publication: The size-change principle for program termination
