Termination proving

VCLA will host a talk by Maria Gorinova on Monday, February 8, 2016.

ABSTRACT

In a world where we increasingly depend more on computers, the need for tools, which can prove the correctness of software has been well established. Termination analysis is central to the process of detecting regions of code which could lead to unresponsiveness of the system. However, proving that a certain program always terminates is hard, especially if this program is very large and complex. One way of tackling this problem is to reason about different parts of the program separately and find conditions for which each of those terminates. This talk presents a method for finding such conditions on termination of a code fragment, which was implemented as a module in the temporal prover T2. The method is based on finding a potential ranking function for the code and then turning that into a valid ranking function by constraining the possible values of the program variables. The inferred preconditions could be used to perform termination analysis on large and complex programs, including interprocedural analysis, interprocedural termination proving, and distributed termination proving.