|1||02-26||Introduction||2007 Turing Award video, 2013 Turing Award video， A Logical Revolution||Slides|
|02-28||SAT I||DP 2|
|03-07||SAT III&BDD||An Introduction to BDDs|
Note: schedule is subject to change.
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..
Project 80% + Participation 20%
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):
We always welcome any feedback on what we could do better. You are also welcome to send us feedback anonymously if you like.