Proving Termination Of Imperative Programs Via Max-SMT Satisfiability Checking Seminar SS 2015

Abstract. Developing reliable programs and proving their total correctness is hard. Not only do we have to prove that they compute ”the right thing”, but we also have to prove that they terminate on a specified, possibly infinite number of inputs. For the latter we present an elegant way to encode the properties of a ranking function and supporting invariants, both being key parts of our termination argument, as a logical formula, thereby transforming our original problem into a satisfiability problem for which efficient solvers exist. Our focus on Max-SMT allows us to retrieve useful information in the case where regular SMT solving would leave us with an inconclusive result, allowing us to refine our formula and continue a better guided termination analysis. Using this approach we can prove a greater number of imperative programs with linear assignments and test conditions than previous approaches with SMT.