• Calendar

November 13, Tuesday
12:00 – 14:00

This talk is about the application of Boolean SAT solvers to the problem of determining program termination. Proving termination is all about the search for suitable ranking functions. The key idea in this work is to encode the search for particular forms of ranking functions to Boolean statements which are satisfiable if and only if such ranking functions exist. In this way, proving termination can be performed using a state-of-the-art Boolean satisfaction solver.

We have applied this approach to several variants of the so-called LPO termination problem which comes up in the context of term rewrite systems. Experimental results are unequivocal, indicating orders of magnitude speedups in comparison with previous implementations for LPO termination. Our results have had a direct impact on the design of several major termination analyzers for term rewrite systems. Moreover, there are an increasing number of new results illustrating additional applications of SAT to proving termination.