CS242: Computer-Aided Verification

Schedule
Week	Date	Topic	Reading	Notes
1	02-26	Introduction	2007 Turing Award video, 2013 Turing Award video， A Logical Revolution	Slides
1	02-28	SAT I	DP 2
2	03-05	SAT II
2	03-07	SAT III&BDD	An Introduction to BDDs
3	03-12
3	03-14
4	03-19
4	03-21
5	03-26
5	03-28
6	04-02
6	04-04
7	04-09
7	04-11
8	04-16
8	04-18
9	04-23
9	04-25
10	04-30
10	05-02
11	05-07
11	05-09
12	05-14
12	05-16

Note: schedule is subject to change.

Description

How can a programmer verify that the software/hardware/protocol (s)he has designed works correctly as intended? Computer-aided verification is a sub-discipline of computer science aimed at developing tools and techniques to assist programmers meet this goal. 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..

References

DP: Decision Procedures: An Algorithmic Point of View (2nd Edition), Daniel KroeningOfer Strichman, Springer, 2016
PMC: Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press, April 2008

Requirements

Reading: Read the papers and chapters before every class.
Participation: participate actively during class .

Grading

Project 80% + Participation 20%

Project

The course project is the most important component of this class. It is expected that students team up in groups of 2 or 3 for their project. It can be a theoretical and/or experimental investigation related to topics covered in class. There should be some new research in it: either a new application (case-studies) of existing formal methods/tools, or a new formal technique, or both. Simply surveys of existing papers without any input of new ideas will not be acceptable. The main deliverables will be: (1) 1-2 page proposal, with precise problem definition, literature survey, and timeline; (2) 5-10 page final report: This should read like a conference paper, must use latex article class in default setting; (3) Project presentation and possibly demo.

We enforce academic integrity strictly. If you participate in any form of cheating, you will fail this course immediately. Examples of cheating on homework include (but are not limited to):