## 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.