_This is a half-semester course offered in the second half of the spring
semester._
The course is an introduction to deductive verification building on the
foundational principles of Hoare logic and extending them to modern
applications of separation logic (state of the art is Facebook's Infer
verifier). Apart from theoretical exercises, we will spend some time working
with Why3 - a tool for deductive program verification.
Topics covered:
* Hoare logic: foundations, formulation for an ML-like language, application to practical (automated) verification of programs
* separation logic: motivation and foundations, possible approaches to automatization, other applications (e.g., in concurrency)
