Inductive reasoning in superposition

Abstract

In this thesis, we focus on extending automated reasoning for formal verification with induction. Theories of inductively defined data types, such as natural numbers or lists, and the theory of integer arithmetic are commonly used in the development of imperative and functional programs. Further, reasoning about loops or recursion often requires the inductive principle. Therefore, automating reasoning in formal verification of programs also needs to automate induction over the types of the aforementioned theories. To adequately respond to the demand of ensuring trustworthiness of software systems, this thesis focuses on (1) mechanizing inductive reasoning within first-order theorem proving, and (2) constructing programs based on first-order proofs possibly using induction. In the first part, we extend the inductive reasoning capabilities for the saturation-based framework of automated first-order theorem provers. The challenge is that the framework substantially differs from most inductive provers – it does not support the goal/subgoal architecture. We therefore integrate induction with the superposition calculus used by the saturation framework, and do not use rewrite rules nor external heuristics for generating auxiliary inductive lemmas. In the second part, we propose a deductive program synthesis framework based on saturation. We use theorem proving as a basis for synthesis from a functional specification given as a first-order formula expressing the existence of a particular program. In the process of proving the existence of a program, we also synthesize the program, which is correct by construction. We begin with constructing recursion-free programs from induction-free proofs, and then we extend this approach to also synthesize simple recursive programs from proofs using induction. We implemented the inductive reasoning techniques described in this thesis in the saturation-based theorem prover Vampire. We present a set of experimental evaluations of our implementation, demonstrating that the approaches proposed in this thesis work well in practice.