A SAT-Based Approach to Size Change Termination with Global Ranking Functions

No abstract is available for this paper.

• Publication year

  2008

• Venue

  International Conference on Tools and Algorithms for Construction and Analysis of Systems

• Publication date

  2008-03-29

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-540-78800-3_16
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Amortised Memory Analysis Using the Depth of Data Structures

  2009cited by this paper
• Ranking Functions for Size-Change Termination II

  2009influential reference
• A complexity tradeoff in ranking-function termination proofs

  2009cited by this paper
• Ranking functions for size-change termination

  2009cited by this paper
• Proving Termination Using Recursive Path Orders and SAT Solving

  2007cited by this paper
• Certified Size-Change Termination

  2007influential reference
• Termination analysis of logic programs through combination of type-based norms

  2007cited by this paper
• Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings

  2007cited by this paper
• Termination proofs for systems code

  2006cited by this paper
• Termination Analysis with Calling Context Graphs

  2006cited by this paper
• Size-Change Termination and Bound Analysis

  2006cited by this paper
• Solving Partial Order Constraints for LPO Termination

  2005cited by this paper
• Termination Analysis of Higher-Order Functional Programs

  2005cited by this paper
• Abstraction Refinement for Termination

  2005cited by this paper
• The size-change principle and dependency pairs for termination of term rewriting

  2005cited by this paper
• Testing for Termination with Monotonicity Constraints

  2005cited by this paper
• Logic Programming

  2004cited by this paper
• Termination Analysis of the Untyped lamba-Calculus

  2004cited by this paper
• Under Consideration for Publication in Theory and Practice of Logic Programming Logic Programming with Satisfiability

  2003cited by this paper
• Call-by-value is dual to call-by-name

  2003cited by this paper
• Program termination analysis in polynomial time

  2002cited by this paper
• The size-change principle for program termination

  2001influential reference
• Noname manuscript No. (will be inserted by the editor) A General Framework for Automatic Termination Analysis of Logic Programs ⋆

  2000cited by this paper
• A Semantic Basis for the Termination Analysis of Logic Programs

  1999influential reference
• TermiLog: A System for Checking Termination of Queries to Logic Programs

  1997cited by this paper
• Proving termination with multiset orderings

  1979cited by this paper

• VDM recursive functions in Isabelle/HOL

  2023cites this paper
• Tuple Interpretations for Termination of Term Rewriting

  2022cites this paper
• Certifying the Weighted Path Order

  2020cites this paper
• Size-based termination of higher-order rewriting

  2018cites this paper
• Fast offline partial evaluation of logic programs

  2014cites this paper
• A unified ordering for termination proving

  2014cites this paper
• Termination analysis with recursive calling graphs

  2014cites this paper
• Automated verification of termination certificates

  2014cites this paper
• The Weighted Path Order for Termination of Term Rewriting

  2014cites this paper
• Termination and cost analysis: Complexity and precision issues

  2013cites this paper
• Unifying the Knuth-Bendix, recursive path and polynomial orders

  2013cites this paper
• Compact Encoding of Model-Based Diagnosis to Boolean Satisfiability

  2012cites this paper
• SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs

  2012cites this paper
• On the Termination of Integer Loops

  2012cites this paper
• SAT encodings: from constraint-based termination analysis to circuit synthesis

  2012cites this paper
• On the Formalization of Termination Techniques based on Multiset Orderings

  2012influential citation
• Bounded Termination of Monotonicity-Constraint Transition Systems

  2012cites this paper
• Monotonicity Constraints for Termination in the Integer Domain

  2011cites this paper
• Certification of Safe Polynomial Memory Bounds

  2011cites this paper
• Size Invariant and Ranking Function Synthesis in a Functional Language

  2011cites this paper
• A Hybrid Approach to Conjunctive Partial Deduction

  2010influential citation
• Lazy Abstraction for Size-Change Termination

  2010influential citation
• A Hybrid Approach to Conjunctive Partial Evaluation of Logic Programs

  2010cites this paper
• Size-Change Termination and Transition Invariants

  2010cites this paper
• Ranking Functions for Size-Change Termination II

  2009influential citation
• A complexity tradeoff in ranking-function termination proofs

  2009cites this paper
• Automating recursive definitions and termination proofs in higher-order logic

  2009cites this paper
• Termination Proofs in Higher-Order Logic

  2009cites this paper
• Ranking functions for size-change termination

  2009cites this paper
• Size-Change Termination, Monotonicity Constraints and Ranking Functions

  2009cites this paper
• A Mechanized Proof Reconstruction for SCNP Termination

  2009influential citation
• Using CLP Simplifications to Improve Java Bytecode Termination Analysis

  2009cites this paper
• Towards Scalable Partial Evaluation of Declarative Programs

  2009cites this paper