_This is a half-semester course offered in the first 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. Apart from theoretical exercises, we will spend some time working with tools, such as 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)
