|
|
|---|
|
|
|
|---|
J. Matthews, J S. Moore, S. Ray and D. Vroon, “
Verification Condition Generation via Theorem Proving”, in
Proceedings of 13th International Conference on Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR 2006), LNCS 4246,
pp. 362-376, 2006.
Relevance: how to conduct inductive assertion-style
proofs from an operational semantics without a verification condition
generator
Abstract
We present a deductive method to convert (i) a formal operational semantics for a given machine language, and (ii) an off-the-shelf theorem prover, into a high assurance verification condition generator (VCG). Our method automatically generates verification conditions from assertions at join points of basic blocks of a program, analogous to those produced by a custom-built VCG. We show how to achieve this with a theorem prover by symbolic simulation on the operational semantics. Thus no separate VCG needs to be implemented for the target language. Furthermore, we can employ the full power of the theorem prover to generate and discharge the verification conditions. Our method can handle both partial and total correctness, and recursive procedures. It is also compositional, in that the correctness of a subroutine needs only be proved once, rather than at each call site. The method has been used to verify several machine-level programs in the ACL2 theorem prover, including the functional correctness of JVM bytecodes for a CBC-mode encryption algorithm.