Verification Tool Design





How to express correctness constraints?
How to express operator intent?