General Information

• Instructor: Santosh Nagarakatte
• When: August 1 - August 5
• Room: To be Announced
• Textbooks: Course will be self-contained. Recommended books are listed below.

Announcements

• 06/28/2013: Mini-course website up

Schedule

• Aug 1, 2013 (3 hrs)
  • Motivation
  • Propositional Logic
  • Natural Deduction
  • SAT solving
• Aug 2, 2013 (3 hrs)
  • First-order logic
  • Quantifiers and reasoning
  • SMT solvers
• Aug 3, 2013 (6 hrs)
  • Pre-conditions and Post conditions
  • Loop invariants, inductive invariants
  • Science of Programming
  • Weakest pre-condition
  • Programming with Dafny, an auto-active program verifier
• Aug 5, 2013 (3 hrs)
  • Proving with Dafny
  • Verified LLVM project

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.