Invariants from Tests in Boogie; Combining Dynamic and Static Testing Methods to identify Loop Invariants of Boogie Programs

Abstract

Proving implementations with loops against their specifications using automatic verifiers, requires annotations in the form of loop invariants. Loop invariants are properties that must hold for every iteration of a loop and identifying them is generally a difficult endeavour. Invariant inference algorithms can assist this process by generating possible invariants and identifying candidate invariants, using static or dynamic testing. This thesis examines how symbolic execution can compensate for the lack of traditional dynamic testing methods in the context of Boogie programs, to identify candidate invariants for such programs using a combination of dynamic and static testing. Boogie is a verification language that combines a typed logic and a simple procedural language; this combination makes Boogie programs not executable in general, which makes applying dynamic analysis techniques challenging. This thesis implements an algorithm for invariant inference that generates possible invariants from templates and post-conditions. The identification of candidate invariants is split into disproving as many wrong invariants as possible, using the symbolic execution engine Boogaloo, and identifying candidate invariants from the remaining set of invariants, by proving them with the Boogie verifier. A detailed analysis, on 15 carefully selected Boogie programs, shows that the combination of dynamic and static testing can be quite powerful, being able to infer invariants sufficient to prove 10 of the 15 programs correct fully automatically. However, the results also suggests a connection between the kinds of possible invariants that are generated and the impact the symbolic execution has on the performance.