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

- Number of participants: We give topics to at most 12 students.
- Target audience: Computer Science students. This is a joint seminar for Bachelor’s and Master’s students.
- Location: Room 1A-502 in SIST building
- Prerequisites: basic knowledge of algorithms, data structures, programming languages, computational complexity, and propositional logic. The course requires mathematical maturity, and is appropriate for students who wish to pursue research in formal methods or programming languages. If you need more information to decide, contact the instructor.

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.

- 07-04, 13:30-15:00, 1A-502: Introduction and Course Overview (by Fu Song)
- [Slides]
- Optional viewing [2007 Turing Award]

- 07-05, 13:30-16:00, 1A-402: SAT Solving (by Yueying Zhang from ECNU)
- 07-11, 10:30-11:30, 1A-200: Model checking quantum Markov chains (Guest Speaker, Yuan Feng)
- 07-12, 13:30-15:00, 1A-402: BDD (by Yedi Zhang)
- 07-13, 13:30:16:30, 1A-502: SMT Part I&II (by Min Zhang from ECNU)
- 07-14, 13:30:16:30, 1A-502: SMT Part III&IV (by Min Zhang from ECNU)
- 07-17, 13:30:16:00, 1A-502: Model Checking and Temporal Logic I (by Yu Tang)
- 07-18, 13:30:16:00, 1A-502: Model Checking and Temporal Logic II (by Yu Tang)
- 07-19, 13:30:16:00, 1A-502: Symbolic Model Checking with BDDs (by Yedi Zhang)
- 07-20, 13:30:16:00, 1A-402: Static analysis: dataflow analysis (by Feng Wang)
- 07-21, 13:30:16:00, 1A-502: Static analysis: abstract interpretation (by Jun Zhang)
- 07-24, 13:30:16:00, 1A-502: Static analysis: interprocedural analysis (by Pengfei Gao)
- 07-25, 13:30:16:00, 1A-502: Static analysis: Concolic testing (by Haifeng Gu)
- [SLides1] [SLides2]
- Mandatory:

(1) CUTE: A Concolic Unit Testing Engine for C

(2) DART: Directed Automated Random Testing - Optional:

(1) Hybrid Concolic Testing

(2) CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools

(3) Concolic Testing

(4) Automated Concolic Testing of Smartphone Apps

- 07-26, 13:30:16:00, 1A-402: Symbolic Model Checking with SAT/SMT (by Fu Song)
- 07-27, 13:30:16:00, 1A-502: Hardware Verification & Software Model Checking
- [Hardware MC slides] [Blast slides]
- Mandatory:

(1) Symbolic Model Checking for Sequential Circuit Verification

(2) Software model checking - Optional:

(1) ASPDAC/VLSI 2002 Tutorial: Functional Verification of System on Chip - Practices, Issues and Challenges

(2) A decade of software model checking in SLAM

(3) SAT-Based Model Checking Without Unrolling

(4) Hardware Design Verification: Simulation and Formal Method-Based Approaches

(5) A Roadmap for Formal Property Verification

(6) Software Model Checking via IC3

- 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]