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:35, 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.

Methods have been proposed to use the operational semantics of machine languages to automatically generate verification condition generators. [1]

  1. ^ "Verification Condition Generation via Theorem Proving" (PDF). {{cite web}}: Unknown parameter |authors= ignored (help); line feed character in |title= at position 33 (help)
Retrieved from "https://en.wikipedia.org/w/index.php?title=Verification_condition_generator&oldid=562123599"