Warning
- This talk is about a manually constructed verification proof.
- In our HCSS04 paper, Dick Kieburtz wrote
The motivation to develop an automatic verification server lies in
the boring nature of verification proofs.
Unlike proofs of interesting mathematical theorems, many of which
are based upon deep insights into the underlying mathematical
structures, and which, once done, become the subject of continued
study and improvement, verification proofs tend to be based upon
shallow theories of superficially complex
structures. Such proofs may not require deep insight, although
they are often highly detailed.
- Be prepared to be bored!