Date Added: Nov 2011
There are two dominant approaches for the construction of automatic program verifiers, Verification Condition Generation (VCG) and Symbolic Execution (SE). Both techniques have been used to develop powerful program verifiers. However, to the best of the authors' knowledge, no systematic experiment has been conducted to compare them. This paper reports on such an experiment. They have used the specification and programming language Chalice and compared the performance of its standard VCG verifier with a newer SE engine called Syxc, using the Chalice test suite as a benchmark.