  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?
