The size-change principle for program termination
From MaRDI portal
Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45)
Recommendations
Cited in
(95)- A complexity tradeoff in ranking-function termination proofs
- Adapting functional programs to higher order logic
- Automata and program analysis
- A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
- Formalization of the computational theory of a Turing complete functional language model
- \textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programs
- Asynchronous unfold/fold transformation for fixpoint logic
- Run-time complexity bounds using squeezers
- Loop summarization using state and transition invariants
- A second-order formulation of non-termination
- Fast offline partial evaluation of logic programs
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- The size-change principle and dependency pairs for termination of term rewriting
- A combination framework for complexity
- Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys
- Type-level computation using narrowing in \(\Omega\)mega
- ACL2s: ``the ACL2 sedan
- On the termination of integer loops
- Stop when you are almost-full. Adventures in constructive termination
- An abstract interpretation framework for termination
- The strength of the SCT criterion
- Loop Summarization and Termination Analysis
- Decision Procedures for Automating Termination Proofs
- Advanced Ramsey-based Büchi automata inclusion testing
- Size-change termination and satisfiability for linear-time temporal logics
- Predicate abstraction for program verification
- Asymptotically precise ranking functions for deterministic size-change systems
- A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
- Size-Change Termination and Bound Analysis
- Call-by-value Termination in the Untyped lambda-calculus
- The Computability Path Ordering: The End of a Quest
- A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs
- Büchi Complementation and Size-Change Termination
- All-Termination(T)
- Ranking Functions for Size-Change Termination II
- Automata-Based Termination Proofs
- scientific article; zbMATH DE number 1953270 (Why is no real title available?)
- scientific article; zbMATH DE number 2018591 (Why is no real title available?)
- scientific article; zbMATH DE number 2043534 (Why is no real title available?)
- scientific article; zbMATH DE number 2084367 (Why is no real title available?)
- Size-based termination of higher-order rewriting
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- Proving termination of nonlinear command sequences
- Verification and code generation for invariant diagrams in Isabelle
- Size-change termination and transition invariants
- Lazy abstraction for size-change termination
- Ramsey's theorem for pairs and \(k\) colors as a sub-classical principle of arithmetic
- An intuitionistic version of Ramsey's theorem and its use in program termination
- scientific article; zbMATH DE number 7453196 (Why is no real title available?)
- Local validity for circular proofs in linear logic with fixed points
- Dependency pairs termination in dependent type theory modulo rewriting
- A tier-based typed programming language characterizing feasible functionals
- On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
- Tight polynomial worst-case bounds for loop programs
- Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic Programs
- Ramsey-based inclusion checking for visibly pushdown automata
- An intuitionistic analysis of size-change termination
- The size-change termination principle for constructor based languages
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- Logic Programming
- Programming Languages and Systems
- Programming Languages and Systems
- Ranking functions for linear-constraint loops
- Proving Termination with (Boolean) Satisfaction
- Termination Analysis of Logic Programs Based on Dependency Graphs
- Termination Analysis with Calling Context Graphs
- Programming Languages and Systems
- Rewriting Techniques and Applications
- Affine-based size-change termination.
- Calculating sized types
- Termination of linear programs with nonlinear constraints
- Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
- PML2: integrated program verification in ML
- 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
- Jeopardy: an invertible functional programming language
- Abstract cyclic proofs
- Termination analysis of programs with multiphase control-flow
- Termination of graph transformation systems via generalized weighted type graphs
- From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
- T-rex: termination of recursive functions using lexicographic linear combinations
- Checking equivalence in a non-strict language
- The size-change principle for mixed inductive and coinductive types
- Totality for mixed inductive and coinductive types
- Cyclic proofs and size-change termination
- Complete and tractable machine-independent characterizations of second-order polytime
- Executable Transitive Closures
- On proving \(C_E\)-termination of rewriting by size-change termination
- Summarization for termination: No return!
- Verifying termination and reduction properties about higher-order logic programs
- Mechanizing and improving dependency pairs
- Partial and nested recursive function definitions in higher-order logic
This page was built for publication: The size-change principle for program termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178875)
