Discovering Invariants by Solving Constraints

One of the best ways to understand a program is to figure out what invariants hold; any program that, on completion, puts an array of numbers into ascending order we would instantly recognise as a sort. Invariants also help us to argue that things to do not go wrong, for example, that an array is always indexed in range or that a loop always terminates. Therefore there has been much interest in automatically discovering invariants. Recently it has been shown how (Boolean) constraint solving can be applied to this problem. The idea is to encode the paths through a program as Boolean constraints, and then repeatedly solve the constraints, so as to enumerate different paths. By confining the invariants to certain classes, it is possible to summarise all paths in a finite number of steps, and hence derive an invariant. It has been shown how this technique enables efficient (Boolean) constraint solvers to be applied to discover invariants that cannot be found by other methods. However, there is no reason why this technique cannot be refined to derive richer invariants by applying different constraint solvers. The PhD studentship will explore this promising thread of work.