2 Verification Conditions for Single-assignment Branching Programs

The use of an intermediate single-assignment form is central in the design of major modern pro-gram verification tools, from deductive verifiers like Boogie and Why3 to automated tools like the CBMC bounded model checker. In this tutorial paper we formalize the program verification tech-nique that consists in the translation of branching code to such an intermediate single-assignment form, from which verification conditions are generated. Soundness and completeness results are established for the technique, and different methods for generating the verification conditions ar