A Hoare-Style Calculus with Explicit State Updates
Reiner Hähnle, Richard Bubel · Chalmers Publication Library (Chalmers University of Technology) · 2008
We present a verification system for a variant of Hoare-logic that supports proving by forward symbolic execution. In addition, no explicit weakening rules are needed and first-order reasoning is automated. The system is suitable for teaching program verification, becaus et he student can concentrate on reasoning about programs following their natural control flow and proofs are machine-checked.