Hoare-Style Program Verification (Lecture 1)
- Rustan Leino
Rob DeLine's CSE 503, Software Engineering, University of Washington, Seattle, WA |
Published by Microsoft Research
Making sense of programs
- Program semantics defines programming language
- e.g., Hoare logic, Dijkstra’s weakest preconditions
- Specifications record design decisions
- bridge intent and code
- Tools amplify human effort
- manage details
- find inconsistencies
- ensure quality