Instructional Video Series
This three video series demonstrates how to formally prove the correctness of a simple operation.
Building a Reasoning Table – demonstrates how to build a reasoning table for a simple operation.
Generating VCs – uses the reasoning table from Video #1 to demonstrate how to generate the verification conditions for the operation.
Proving VCs – demonstrates how to prove the correctness of the operation by proving the verification conditions generated in Video #2.