SAT Solving for Termination Analysis with Polynomial Interpretations

DOI10.1007/978-3-540-72788-0_33zbMath1214.68352OpenAlexW1484559376MaRDI QIDQ3612476

Peter Schneider-Kamp, Carsten Fuhs, Aart Middeldorp, Harald Zankl, René Thiemann, Jürgen Giesl

Publication date: 10 March 2009

Published in: Theory and Applications of Satisfiability Testing – SAT 2007 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-72788-0_33

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (34)

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Optimization modulo non-linear arithmetic via incremental linearization ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ KBO orientability ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Size-based termination of higher-order rewriting ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ Constraint-based correctness proofs for logic program transformations ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Maximal Termination ⋮ Usable Rules for Context-Sensitive Rewrite Systems ⋮ Proving Quadratic Derivational Complexities Using Context Dependent Interpretations ⋮ Root-Labeling ⋮ Automated Implicit Computational Complexity Analysis (System Description) ⋮ Automated Complexity Analysis Based on the Dependency Pair Method ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ Empirical Study of the Anatomy of Modern Sat Solvers ⋮ Monotonicity Criteria for Polynomial Interpretations over the Naturals ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Proving Termination of Integer Term Rewriting ⋮ Dependency Pairs and Polynomial Path Orders ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Increasing interpretations ⋮ Proving Termination with (Boolean) Satisfaction ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ Search Techniques for Rational Polynomial Orders ⋮ Increasing Interpretations

Uses Software

• MiniSat
• Pueblo
• Tyrolean
• AProVE

This page was built for publication: SAT Solving for Termination Analysis with Polynomial Interpretations