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 seminar 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.
During the summer term 2017/18, System safety and security lab(S3L) offers a seminar on computer-aided verification, headed by Prof. Fu Song. If you are interested in participating, please drop me a message with a motivation letter. Application Deadline: 30 June, 23:59:59
Each course topic will have associated readings, and some topics will involve reading and critiquing current research papers. Therefore, all students have to read the associated readings before each lecture, attend the lectures and participate in class discussion. Each lecture will be hosted by one of you.
There is no credit for this seminar.
Note: schedule is subject to change.
 Model Checking, Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, MIT Press,January 2000
 Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, Cambridge University Press, June 2004 (2nd edition) [Tell Fu Song if you need]
 The Calculus of Computation: Decision procedures with applications to verification, Aaron Bradley and Zohar Manna, Springer, 2007 [PDF]
 Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press, April 2008 [PDF]
 Decision Procedures: An Algorithmic Point of View, Daniel Kroening, Ofer Strichman, Springer, 2008 [PDF]