Towards Automating Induction for Software Verification - Guiding Inductive Reasoning in Superposition-based Theorem Proving

Abstract

This thesis explores automating inductive reasoning for software verification of programs containing loops, arrays and recursive function calls. We propose new methods of automating induction in first-order theorem proving based on the superposition calculus allowing forfully automated verification using theorem proving for such programs. In the first part of the thesis, we explore induction in trace logic, an instance of many-sorted first-order logic with theories. We propose two methodologies to handle inductive loop reasoning in trace logic and implement our work in the RAPID verification framework and the underlying saturation prover VAMPIRE. In our first approach, we extend trace logic program semantics with so-called trace lemmas. Trace lemmas express common properties over programs with loops, integers and unbounded arrays based on bounded induction over timepoints. We identify a set of trace lemmas for such programs. These lemmas help the automated theorem prover with inductive reasoning and enable the full automation of proofs of such programs. Furthermore, we reduce reliance on trace lemmas by introducing bounded induction over timepoints directly in the underlying theorem prover. That is, we extend the saturation-based prover with two inductive inferences specific to reasoning in trace logic, namely multi-clause goal induction and array mapping induction, for lemmaless reasoning over loop iterations. Both inference rules enable the prover to derive safety properties over programs with loops, arrays and integers without the need of a priori trace lemma reasoning.The second part of the thesis deals with program semantics and inductive reasoning for recursive programs. Specifically, we formalize functional program semantics in many-sorted first order logic and showcase our approach by proving common sorting algorithms correct. To this end, we extend the saturation prover VAMPIRE with specific structural induction rules based on lists parameterized by any sort that allows for a linear order, namely computation induction. Based on this methodology we provide a fully automated correctness proof of the recursive Quicksort algorithm among other sorting algorithms.