Analysis of Iterative or Recursive Programs Using a First-Order Theorem Prover
Simon Robillard · Chalmers Publication Library (Chalmers University of Technology) · 2016
Static analysis of program semantics can be used to provide strong guarantees about the correctness of software systems. In this thesis, we explore ways to perform automated program analysis and verification using a first-order theorem prover.First we present an extension to the symbol elimination technique for automatic generation of loop invariants. This extensionintroduces a new input format intended to act as an intermediate verification language, facilitating the analysis of programs writtenin a variety of languages. It also integrates program annotations (pre- and post-conditions), so that symbol elimination can be used notonly to generate invariant, but also to prove the correctness of programs independently of other tools.We then present ways to perform complete reasoning in the theory of term algebras in a first-order theorem prover. As term algebrasprovide a concrete semantics for values of algebraic data types, this extension enables one to reason about programs manipulating such data types, in particular in functional languages.Both works were implemented using the first-order theorem prover Vampire; these implementations are presented along with experiments on difficult verification problems.