Formally Validating a Practical Verification Condition Generator (extended version)

Gaurav Parthasarathy, Peter Müller, Alexander J. Summers

A program verifier produces reliable results only if both the logic used to justify the program's correctness is sound, and the implementation of the program verifier is itself cor…