Strongest postcondition of unstructured programs

Abstract

To avoid exponential explosion, program verifiers turn the program into a passive form before generating verification conditions. A little known fact is that the passive form makes it easy to use a strongest postcondition calculus to derive the verification condition. In the first part of this paper, the passivation phase is defined precisely enough to allow a study of its algorithmic properties. In the second part, the weakest precondition and strongest postcondition methods are presented in a unified way and then compared empirically.