Jump to content

Verification condition generator

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Eptified (talk | contribs) at 15:32, 29 June 2013. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

A verification condition generator is a sub-component of a program verifier that synthesizes formal verification conditions by analyzing a program's source code using a method based upon Hoare logic. VC generators may require that the source code contains logical annotations such as pre/post-conditions and loop invariants. VC generators are often coupled with SMT solvers in the backend of a program verifier. After a verification condition generator has created the verification conditions they are passed to an automated theorem prover, which is another component of a program verifier.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Verification_condition_generator&oldid=562123268"