 Verification condition generator

A Verification Condition Generator (VCG) is a tool used primarily in formal verification, which is a method for ensuring the correctness of hardware and software systems. The main purpose of a VCG is to take a program or system specification and generate verification conditions (VCs) that must be satisfied for the program to be considered correct according to its specification.