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

DOI10.1007/978-3-540-78800-3_16MaRDI QIDQ5458329zbMATH OpenOpenAlexFDO

Authors Michael Codish, Amir M. Ben-Amram

Publication date 11 April 2008

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78800-3_16

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Ranking Functions for Size-Change Termination II
• Size-change termination, monotonicity constraints and ranking functions
• Lazy abstraction for size-change termination
• Size-Change Termination, Monotonicity Constraints and Ranking Functions
• A complexity tradeoff in ranking-function termination proofs

Cites work

• A general framework for automatic termination analysis od logic programs
• A semantic basis for the termination analysis of logic programs
• Certified Size-Change Termination
• Logic Programming
• Logic programming with satisfiability
• Programming Languages and Systems
• Proving Termination Using Recursive Path Orders and SAT Solving
• Proving termination with multiset orderings
• Ranking Functions for Size-Change Termination II
• Rewriting Techniques and Applications
• Size-Change Termination and Bound Analysis
• Solving Partial Order Constraints for LPO Termination
• Static Analysis
• Termination Analysis with Calling Context Graphs
• The size-change principle and dependency pairs for termination of term rewriting
• The size-change principle for program termination

Cited in

(11)

• A complexity tradeoff in ranking-function termination proofs
• Tuple interpretations for termination of term rewriting
• SAT solving for termination proofs with recursive path orders and dependency pairs
• Fast offline partial evaluation of logic programs
• A hybrid approach to conjunctive partial evaluation of logic programs
• Ranking Functions for Size-Change Termination II
• Size-based termination of higher-order rewriting
• Lazy abstraction for size-change termination
• Proving Termination with (Boolean) Satisfaction
• Size-change termination, monotonicity constraints and ranking functions
• Certifying the weighted path order (invited talk)

This page was built for publication: A SAT-Based Approach to Size Change Termination with Global Ranking Functions

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