Summer Seminar: Computer-Aided Verification, 2017/18


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.


  1. 07-04, 13:30-15:00, 1A-502: Introduction and Course Overview (by Fu Song)
  2. 07-05, 13:30-16:00, 1A-402: SAT Solving (by Yueying Zhang from ECNU)
  3. 07-11, 10:30-11:30, 1A-200: Model checking quantum Markov chains (Guest Speaker, Yuan Feng)
  4. 07-12, 13:30-15:00, 1A-402: BDD (by Yedi Zhang)
  5. 07-13, 13:30:16:30, 1A-502: SMT Part I&II (by Min Zhang from ECNU)
  6. 07-14, 13:30:16:30, 1A-502: SMT Part III&IV (by Min Zhang from ECNU)
  7. 07-17, 13:30:16:00, 1A-502: Model Checking and Temporal Logic I (by Yu Tang)
  8. 07-18, 13:30:16:00, 1A-502: Model Checking and Temporal Logic II (by Yu Tang)
  9. 07-19, 13:30:16:00, 1A-502: Symbolic Model Checking with BDDs (by Yedi Zhang)
  10. 07-20, 13:30:16:00, 1A-402: Static analysis: dataflow analysis (by Feng Wang)
  11. 07-21, 13:30:16:00, 1A-502: Static analysis: abstract interpretation (by Jun Zhang)
  12. 07-24, 13:30:16:00, 1A-502: Static analysis: interprocedural analysis (by Pengfei Gao)
  13. 07-25, 13:30:16:00, 1A-502: Static analysis: Concolic testing (by Haifeng Gu)
  14. 07-26, 13:30:16:00, 1A-402: Symbolic Model Checking with SAT/SMT (by Fu Song)
  15. 07-27, 13:30:16:00, 1A-502: Hardware Verification & Software Model Checking
  16. 07-28, 13:30:16:00, 1A-502: Protocol Model Checking (by Yao Zeng)

Note: schedule is subject to change.


[1] Model Checking, Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, MIT Press,January 2000
[2] 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]
[3] The Calculus of Computation: Decision procedures with applications to verification, Aaron Bradley and Zohar Manna, Springer, 2007 [PDF]
[4] Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press, April 2008 [PDF]
[5] Decision Procedures: An Algorithmic Point of View, Daniel Kroening, Ofer Strichman, Springer, 2008 [PDF]