CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Analysis of Iterative or Recursive Programs Using a First-Order Theorem Prover

Simon Robillard (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Gothenburg : Chalmers University of Technology, 2016.
[Licentiatavhandling]

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 extension
introduces a new input format intended to act as an intermediate verification language, facilitating the analysis of programs written
in a variety of languages. It also integrates program annotations (pre- and post-conditions), so that symbol elimination can be used not
only 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 algebras
provide 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.

Nyckelord: Program Verification, Automated Theorem Proving, Invariant Generation, Term Algebras



Denna post skapades 2016-11-07. Senast ändrad 2016-11-14.
CPL Pubid: 244813

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Data- och informationsvetenskap
Programvaruteknik

Chalmers infrastruktur

Examination

Datum: 2016-12-08
Tid: 10:00
Lokal: HC2, Hörsalvägen 14, Chalmers
Opponent: Nikolaj Bjorner, Microsoft Research, USA