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




Related Items (61)

\textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programsRamsey-Based Inclusion Checking for Visibly Pushdown AutomataA combination framework for complexityOn the Termination of Integer LoopsOn proving \(C_E\)-termination of rewriting by size-change terminationSize-Change Termination and Satisfiability for Linear-Time Temporal LogicsPredicate Abstraction for Program VerificationSummarization for termination: No return!Verifying termination and reduction properties about higher-order logic programsAsymptotically Precise Ranking Functions for Deterministic Size-Change SystemsAsynchronous unfold/fold transformation for fixpoint logicMechanizing and improving dependency pairsTermination of linear programs with nonlinear constraintsSize-based termination of higher-order rewritingOn Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational SemanticsMechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofsParameterized recursive refinement types for automated program verificationDistributing and parallelizing non-canonical loopsFormal verification of termination criteria for first-order recursive functionsAbstract cyclic proofsComplete and tractable machine-independent characterizations of second-order polytimeFast offline partial evaluation of logic programsUnnamed ItemUnnamed ItemThe Strength of the SCT CriterionThe Computability Path Ordering: The End of a QuestProving termination of nonlinear command sequencesVerification and code generation for invariant diagrams in IsabelleLoop Summarization and Termination AnalysisEnhancing dependency pair method using strong computability in simply-typed term rewritingRun-time complexity bounds using squeezersA Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification TreesAn intuitionistic version of Ramsey's theorem and its use in program terminationLoop summarization using state and transition invariantsPartial and nested recursive function definitions in higher-order logicUnnamed ItemUnnamed ItemUnnamed ItemEfficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable KeysA Transformational Approach to Polyvariant BTA of Higher-Order Functional ProgramsBüchi Complementation and Size-Change TerminationAll-Termination(T)A SAT-Based Approach to Size Change Termination with Global Ranking FunctionsDecision Procedures for Automating Termination ProofsA complexity tradeoff in ranking-function termination proofsEfficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic ProgramsUnnamed ItemA novel learning algorithm for Büchi automata based on family of DFAs and classification treesAdvanced Ramsey-Based Büchi Automata Inclusion TestingAutomata-Based Termination ProofsRAMSEY’S THEOREM FOR PAIRS ANDKCOLORS AS A SUB-CLASSICAL PRINCIPLE OF ARITHMETICAdapting functional programs to higher order logicRanking Functions for Linear-Constraint LoopsUnnamed ItemProving Termination with (Boolean) SatisfactionTermination Analysis of Logic Programs Based on Dependency GraphsThe size-change principle and dependency pairs for termination of term rewritingFormalization of the computational theory of a Turing complete functional language modelType-level Computation Using Narrowing in ΩmegaACL2s: “The ACL2 Sedan”A second-order formulation of non-termination




This page was built for publication: The size-change principle for program termination