Automated software verification using superposition-based theorem proving

Abstract

This thesis explores the automated verification of software programs involving loops and arrays using superposition-based theorem proving. It proposes new techniques at the intersection of program semantics, software verification, and automated reasoning. In the first part of the thesis, we introduce an expressive instance of first-order logic modulo theories, called trace logic. We present a sound and complete axiomatic semantics of software programs and use it to capture the partial correctness of program properties as validity statements in trace logic. Our semantics describes each timepoint in the execution of a program uniquely and keeps program locations explicit. We then introduce a verification framework, which handles the inductive reasoning needed in the trace logic domain in order to enable off-the-shelf first-order theorem provers to reason about validity statements in trace logic. Our framework adds instances of an expressive induction axiom scheme explicitly into the search space, in contrast to other approaches which use induction axioms only on the meta- level. We then discuss how the combination of explicit induction axioms and backward-reasoning enables automated loop splitting, which is the key for verifying advanced array-properties. We conclude the first part of the thesis by generalizing the trace-logic-based verification framework to support multiple execution traces and relational properties. In the second part of the thesis, we apply superposition-based theorem proving, and in particular the state-of-the-art theorem prover VAMPIRE, to reason about the validity statements of the trace logic domain. We introduce two techniques, layered clause selection and subsumption demodulation, which are crucial for efficient superposition-based reasoning in the trace logic domain. Moreover, to ease the manual analysis of both proofs and failed proof attempts, we describe a tool, which interactively visualizes proof attempts of saturation-based theorem provers. Finally, we provide an experimental evaluation of the trace-logic-based verification framework on interesting sets of benchmarks, which cover challenging properties of software programs including loops and arrays. The presented results suggest that our superposition-based verification framework is an interesting alternative to existing SMT-based verification approaches.