The Design and Algorithms of a Verification Condition Generator
It addresses incremental improvements in program verification tools for developers and researchers.
This dissertation tackles problems related to verification condition generators, including formalizing transformations into pure functional languages, relating semantics descriptions, enabling incremental verification, and detecting unreachable code with formal specifications, but does not provide concrete numerical results.
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?