Doctoral Thesis Defense - Claúdio Filipe Belo da Silva Lourenço

Date: 
Monday, July 2, 2018, 4:11pm

Title: Single-assignment Program Verification

Abstract: Many program verification tools rely on the translation of code annotated with properties into an intermediate single-assignment form (in a more or less explicit way), and then on an algorithm that generates verification conditions from it. In this thesis, we revisit two major methods that are widely used to produce verification conditions for single-assignment programs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify di↵erent aspects in which the methods di↵er and show that they can be combined to produce new hybrid verification condition generators; together with the initial algorithms they form what we call the VCGen cube, which we propose as a framework for synthesizing and comparing verification condition generators. Optimizations implemented by verification tools are then integrated into the cube.

At the theoretical level we propose two fully proved verification frameworks based on the translation into single-assignment and subsequent generation of verification conditions. On one hand we formalize program verification based on the translation of While programs annotated with loop invariants into an iterating single-assignment language with a dedicated iterating construct. Soundness and completeness proofs are given for the entire workflow, including the translation of annotated programs into iterating single-assignment form. The formalization is based on a program logic that we show to be adaptation-complete.

On the other hand we formally define an iteration-free single-assignment language with assume, assert, and exceptions, and introduce a program logic for this language which allows us to prove the soundness and completeness of the VCGen cube. A verification framework based on the translation of programs into (iteration-free) single-assignment form is then proposed, and the entire workflow is proved to be sound and complete. We also suggest a concrete singleassignment translation that transforms annotated loops into assumes and asserts to check that the annotated invariants are valid and preserved during the iterations.

Finally, we compare the verification condition generators empirically, both for programs of the LLVM intermediate representation (a concrete popular intermediate language that is based on SA form), and in the context of the Why3 deductive verification tool. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting trends.

Jury: - Rector of the University of Minho

        - Doctor Jorge Miguel Matos Sousa Pinto (Universidade do Minho)

        - Doctor Simão Melo de Sousa (Universidade da Beira Interior)

        - Doctor Gabriel de Sousa Torcato David (Universidade do Porto)

        - Doctor Maria João Gomes Frade (Universidade do Minho)

        - Doctor João Fernando Peixoto Ferreira (Teesside University)

        - Doctor  Claude Marché (INRIA)

Location: Atos Room - Campus de Azurém - Universidade do Minho - Guimarães

Photo: