Verification conditions for single-assignment programs

A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this paper we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms, and propose a uniform presentation of the corresponding sets of VCs, in terms of (logical encodings of) paths in the control-flow graph of a single-assignment form of the program under analysis. This allows us to compare the mechanisms, in particular with respect to the size of the generated formulas.Fundação para a Ciência e a Tecnologia (FCT)This work was partially supported by the following projects funded by Fundação para a Ciência e Tecnologia (FCT): FAVAS (PTDC/EIA-CCO/105034/2008), CROSS (PTDC/EIA-CCO/108995/2008