A verification condition generator is a common sub-component of an automated program verifier that synthesizes formal verification conditions by analyzing a program's source code using a method based upon

Hoare logic Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and lo ...

. VC generators may require that the source code contains logical annotations provided by the programmer or the compiler such as pre/post-conditions and loop invariants (a form of

proof-carrying code Proof-carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can quickly verify the validity of the pro ...

). VC generators are often coupled with

SMT solver In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvin ...

s 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 Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ma ...

, which can then formally prove the correctness of the code. Methods have been proposed to use the

operational semantics Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execut ...

of machine languages to automatically generate verification condition generators.

References

Formal methods {{Computer-science-stub