Course Objectives, Requirements & Contents:

This course is an introduction to the theory and applications of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems. At its core, formal methods is about proof: formulating specifications that form proof obligations, designing systems to meet those obligations, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. In particular, the course will cover topics such as model checking and Boolean satisfiability (SAT) solving.

The course material has applications to several areas including computer security, software engineering, embedded/cyber-physical systems, control systems, robotics, networking and distributed systems, education, systems and synthetic biology, and CAD for integrated circuits. We will therefore focus on fundamental theory and techniques that apply broadly to many systems.

A tentative list of topics to be covered:

SAT & BDDs: Complexity, modern DPLL SAT solvers, Binary Decision Diagrams, BDD representation and manipulation algorithms, applications.

Model Checking: Modeling with finite automata, Kripke structures and extended finite automata.

Temporal logic

Explicit-state model checking

Partial-order reduction

Basic fixpoint theory

Symbolic model checking

Abstraction

Bounded model checking.  

Credits: 2