Program logics and verification

Logics for proving programs correct: Hoare logic for partial and total correctness with soundness and relative completeness, weakest preconditions, verification-condition generation, and separation logic.

• Hoare logic
• Kleene algebra with tests
• Separation logic
• Verification-condition generation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.