Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language
A formalization of B3 ’s semantics, a VC Generator for the language, and a soundness proof that these two correspond are presented, which is a methodology to split the IVL’s semantic encodings into two layers of abstraction to cover realistic aspects of the semantics, while keeping the proofs amenable to automation.