Strongest postcondition of unstructured programs
Radu Gheorghe Grigore, Julien Charles, Fintan Fairmichael, Joseph R. Kiniry · 2009
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.