Mini-Course on Robust Software with Verified Programming

General Information

Announcements

Schedule

Course Description

This course introduces the use of formal methods to develop programs correct by construction (also known as certified software). Certified software consists of a machine-executable program plus a formal machine checked proofs that the software is free of bugs with respect to its specification. Recent success stories in building such certified software include a custom verified Compiler (CompCert), verified microkernels (Verve and Sel4), Verified LLVM Compiler (Vellvm), certified native client interface checker (RockSalt), and many others. Recent advances in automated theorem proving tools and techniques, SMT solvers and SAT solvers makes this feasible. In this course, we will discuss and understand the fundamentals of these techniques and use Dafny (a tool from Microsoft Research) to construct and prove programs.

Course Objectives

This course will motivate students to build correct by construction programs with the help of interactive and automatic theorem provers.

Reading List

Although the mini-course will be self-contained, these are some reference books and papers. Students are encouraged to read them to gain more proficiency.

Books

  • Science of Programming, David Gries, 1981
  • Discipline of Programming, Dijkstra, 1976
  • The Calculus of Computation, Decision Procedures with Applications to Verification, 2007

Papers and tools

  • Formal Verified Compiler Backend -- Journal of Automated Reasoning