View article

Automatic software verification is an important but hard problem. Verifiers primarily rely on static analysis to reason about all possible program behaviors, where a purely static analysis makes inferences based solely on program text. However, since verification is so hard, to be successful it seems necessary to leverage all possible sources that can provide any useful information about the program. Hence, limiting a verifier to just the program text is unnecessarily restrictive. Our thesis is that verification can be aided and significantly improved by learning from data gathered from program executions. In particular, we focus on the problem of invariant inference and its applications in verification. Invariant inference is a core problem that every software verifier must address. The traditional verifiers infer invariants by analyzing program text alone. The main contribution of this thesis is an effective technique to infer loop …