The course Introduction to (semi) automated Software Certification is intended to present the basic concepts of program verification, using formal methods and static analysis techniques. The course will focus on the assertion method, formerly introduced by Floyd and Hoare and developed over fifty years by academic researchers, recently reaching maturity to be of use to certify industrial software.
The course is conceived as a laboratory, directly experimenting with theory by working through examples, using the verification-aware programming language Dafny™, ideated and implemented by K. Rustan Leino, which is at the same time a programming language, a specification language, and an interactive tool to verify programs statically.