Prover Approximations

In order to check programs in an acceptable amount of time, the Prover simplifies the code being verified. This section describes the mechanisms for simplification.


The approximations described in this section may be underapproximations, meaning that they can cause real bugs to be overlooked by the Prover.