The Design and Algorithms of a Verification Condition Generator

TL;DR

This dissertation explores the design and algorithms of a verification condition generator, focusing on formal transformations, semantic descriptions, incremental verification, and unreachable code detection within the Boogie language framework.

Contribution

It introduces formal methods for verification condition generation, analyzes semantic models, and proposes techniques for incremental verification and unreachable code detection.

Findings

Formalization of passive form transformation and its complexity

Relationships between predicate transformers and operational semantics

Techniques for incremental verification and unreachable code detection

Abstract

This dissertation discusses several problems loosely related, because they all involve a verification condition generator. The Boogie language is introduced; the architecture of a verification-generator is described. Then come more interesting parts. (1) Moving to a passive form representation can be seen as an automatic transformation into a pure functional language. How to formalize this transformation and what is its complexity? (2) How do various ways of describing the semantics of procedural languages (predicate transformers, operational semantics) relate to each other? (3) How to do incremental verification? That is, how to work less when re-verifying a program that changed only a little since the verifier was last run. (4) How to detect unreachable code, taking into account formal specifications?