Automated Software Verification with First-Order Theorem Provers

Progress summary of recent developments and results on our work with trace logic and the Rapid verification framework.

Final Report summarizing developments of automating verification with first-order theorem provers

Final Summary

We present a novel approach to automate the verification of first-order inductive program properties capturing the partial correctness of imperative program loops with branching, integers and arrays. We rely on trace logic, an instance of first-order logic with theories, to express first-order program semantics by quantifying over program execution timepoints. Program verification in trace logic is translated into a first-order theorem proving problem where, to date, effective reasoning has required the introduction of so-called trace lemmas to establish inductive properties. In this work, we extend trace logic with generic induction schemata over timepoints and loop counters, reducing reliance on trace lemmas. Inferring and proving loop invariants becomes an inductive inference step within superposition-based first-order theorem proving. We implemented our approach in the Rapid framework, using the first-order theorem prover Vampire. Our extensive experimental analysis shows that automating inductive verification in trace logic is an improvement compared to existing approaches.

We present the Rapid framework for automatic software verification by applying first-order reasoning in trace logic. Rapid establishes partial correctness of programs with loops and arrays by inferring invariants necessary to prove program correctness using a saturation-based automated theorem prover. Rapid can heuristically generate trace lemmas, common program properties that guide inductive invariant reasoning. Alternatively, Rapid can exploit nascent support for induction in modern provers to fully automate inductive reasoning without the use of trace lemmas. In addition, Rapid can be used as an invariant generation engine, supplying other verification tools with quantified loop invariants necessary for proving partial program correctness.

We present a reasoning framework in support of software quality assurance, allowing us to automatically verify the functional correctness of programs with recursive data structures. Specifically, we focus on functional programs implementing sorting algorithms. We formalize the semantics of recursive programs in many-sorted first-order logic while introducing sortedness/permutation properties as part of our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and, hence, concrete sorts. Software validation is powered by automated theorem proving: we adjust recent efforts for automating inductive reasoning in saturation-based first-order theorem proving. Importantly, we advocate a compositional reasoning approach for fully automating the verification of functional programs implementing and preserving sorting and permutation properties over parameterized list structures. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort; to this end, we turn first-order theorem proving into an automated verification engine by guiding automated inductive reasoning with manual proof splits.