Proving Termination with (Boolean) Satisfaction

DOI10.1007/978-3-540-78769-3_1zbMath1179.68034OpenAlexW2177928386MaRDI QIDQ5504589

Michael Codish

Publication date: 22 January 2009

Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

A New Approach to Non-termination Analysis of Logic Programs

Uses Software

• Sat4j
• Tyrolean
• AProVE
• TPDB

Cites Work

• Orderings for term-rewriting systems
• On recursive path ordering
• Termination of rewriting
• Termination of term rewriting using dependency pairs
• Proving Termination Using Recursive Path Orders and SAT Solving
• Solving Partial Order Constraints for LPO Termination
• Termination of String Rewriting with Matrix Interpretations
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Matrix Interpretations for Proving Termination of Term Rewriting
• The size-change principle for program termination
• Computer Aided Verification
• SAT Solving for Argument Filterings
• Satisfying KBO Constraints
• Logic programming with satisfiability
• A machine program for theorem-proving
• Term Rewriting and Applications
• Programming Languages and Systems

This page was built for publication: Proving Termination with (Boolean) Satisfaction