Hoare-Style Program Verification (Lecture 0)

  • Rustan Leino

Rob DeLine's CSE 503, Software Engineering, University of Washington, Seattle, WA |

Published by Microsoft Research

Publication

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