WST on Wednesday, August 16th

Invited Talk (09:30‑10:30)

09:30‑10:30

Yuri Gurevich (Microsoft Research Redmond) Program termination and well partial orderings [ppt] The following known observation may be useful in establishing program termination: if a transitive relation R is covered by finitely many well-founded relations U1, ..., Un then R is well-founded. A question arises how to bound the ordinal height |R| of the relation R in terms of the ordinals αi = |Ui|. We introduce the notion of the stature ||P|| of a well partial ordering P and show that |R| ≤ ||α1 * ... * αn||. Furthermore, this bound is tight; the equality is achieved in some cases. The notion of stature is of considerable independent interest. We define ||P|| as the ordinal height of the forest of nonempty bad sequences of P, but it has many other natural and equivalent definitions. In particular, ||P|| is the supremum, and in fact the maximum, of the lengths of linearizations of P. And ||α1 * ... * αn|| is equal to the natural product α1 ⊗ ... ⊗ αn. Coming back to the question above, we have that |R| ≤ α1 ⊗ ... ⊗ αn, and the bound is tight.

Break (10:30‑11:00)

Session 5: SAT Encoding (11:00‑12:30)

11:00‑11:30	Harald Zankl (University of Innsbruck) Nao Hirokawa (University of Innsbruck) Aart Middeldorp (University of Innsbruck) Constraints for Argument Filterings Argument filterings are a key ingredient of the dependency pair method. Finding a suitable argument filtering that enables the constraints originating from the dependency pair method to be solved by a strictly monotone base order is a challenging search problem. In this note we propose a simple encoding of argument filterings in propositional logic which can be easily combined with propositional encodings of simplification orders, resulting in a propositional formula with the property that any satisfying assignment corresponds to an argument filtering and the parameters of the encoded order which solve the constraints and vice-versa. In order to test the effectiveness of our approach, we implemented the combination with the embedding order on top of the recursive SCC algorithm of Hirokawa and Middeldorp. For satisfiability checking we use two different methods, the state-of-the-art SAT solver MiniSat and a simple OCaml package for manipulating OBDDs. The results are compared with the divide and conquer algorithm implemented in TTT.
11:30‑12:00	Harald Zankl (University of Innsbruck) Aart Middeldorp (University of Innsbruck) KBO as a Satisfaction Problem This note presents an approach to prove termination of term rewrite systems (TRSs) with the Knuth-Bendix order efficiently. The constraints for the weight function as well as for the precedence are encoded in propositional logic and the resulting formula is tested for satisfiability. Any satisfying assignment represents a weight function and a precedence such the induced Knuth-Bendix order orients the rules of the encoded TRS from left to right.
12:00‑12:30	Michael Codish (Ben-Gurion University) Peter Schneider-Kamp (RWTH Aachen) Vitaly Lagoon (University of Melbourne) Rene Thiemann (RWTH Aachen) Juergen Giesl (RWTH Aachen) Automating Dependency Pairs Using SAT Solvers Recent results provide a propositional encoding for lexicographic path orders (LPOs) which facilitates the application of SAT solvers for termination analysis of term rewrite systems. Using this encoding as a black-box together with dependency pairs is not very efficient. Therefore, in this paper we investigate a new combined encoding of LPO in connection with dependency pairs. This new encoding solves two main issues: the combined search for a LPO together with an argument filtering to orient a set of inequalities, and how the choice of the argument filtering influences the set of inequalities that have to be oriented. We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our new encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.

Lunch break (12:30‑14:00)

Session 6: Applications (14:00‑15:30)

14:00‑14:30	Matt Kaufmann (University of Texas) Panagiotis Manolios (Georgia Tech) J Strother Moore (University of Texas at Austin) Daron Vroon (Georgia Institute of Technology, College of Computing) Integrating CCG Analysis into ACL2 ACL2 is a powerful, industrial strength theorem proving system, which has been used on numerous verification pro jects. It is part of the Boyer-Moore family of provers, for which its authors received the 2005 ACM Software System Award. Termination plays a central role in ACL2’s logic. It is used to demonstrate the logical consistency of function definitions and allows for the admission of an induction scheme that mirrors each function’s recursive structure. In previous work we introduced calling context graphs (CCGs) and showed how they can be combined with theorem proving queries to provide a powerful method for proving termination of programs written in first order, functional programming languages. In this paper we describe work we are doing to integrate CCG-based termination analysis into ACL2.
14:30‑15:00	Frederic Blanqui (INRIA) Adam Koprowski (Eindhoven University of Technology) Solange Coupet-Grimal (Université de Provence, Aix-Marseille I) William Delobel (Université de Provence, Aix-Marseille I) Sebastien Hinderer (LORIA) CoLoR, a Coq library on Rewriting and termination Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.
15:00‑15:30	Johannes Waldmann (HTWK Leipzig, FB IMN) Free SCC Analysis via Constant Interpretations We show how to split a (relative) top termination problem into independent subproblems, by using interpretations that are constant on strict rules. This can typically be applied to top termination problems that arise from the dependency pair transformation. The method is applied in the termination prover Matchbox.

Break (15:30‑16:00)

Session 7: Ordinals and Growth (16:00‑16:30)

16:00‑16:30

Andreas Weiermann (Utrecht University, Mathematical Institute) Phase transition phenomena in the context of termination problems We consider parameterized assertions about termination such that for small parameters the resulting complexity is low and for large parameters the resulting complexity is high. In this context one is interested in the phase transition threshold for the transition from low to high complexity. We survey various results which have been obtained in the last years.

System Demonstrations (16:30‑18:30)