Summer Seminar: Computer-Aided Verification, 2017/18

• • Description
  • Organisation
  • Requirements
  • Topics
  • Books

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

Organisation

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.

Requirements

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.

Topics

1. 07-04, 13:30-15:00, 1A-502: Introduction and Course Overview (by Fu Song)
   • [Slides]
   • Optional viewing [2007 Turing Award]
2. 07-05, 13:30-16:00, 1A-402: SAT Solving (by Yueying Zhang from ECNU)
   • [Slides]
   • Mandatory:
     (1) An extensible SAT-solver
   • Optional:
     (1) Boolean Satisfiability Solvers and Their Applications in Model Checking
     (2) Bounded Model Checking Using Satisfiability Solving
     (3) Graph Neural Networks and Boolean Satisfiability
     (4) Deep Network Guided Proof Search
3. 07-11, 10:30-11:30, 1A-200: Model checking quantum Markov chains (Guest Speaker, Yuan Feng)
   • [Slides]
4. 07-12, 13:30-15:00, 1A-402: BDD (by Yedi Zhang)
   • Mandatory:
     (1) An Introduction to Binary Decision Diagrams
   • Optional:
     (1) Lecture Notes on Binary Decision Diagrams
     (2) Boolean Algebra and Binary Decision Diagrams
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)
   • [Slides]
   • Mandatory:
     (1) Satisfiability Modulo Theories
   • Optional:
     (1) Chapters 1-4 and 7-11 of The Calculus of Computation: Decision procedures with applications to verification
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)
   • Slides
   • Mandatory:
     (1) Chapters 4-6 of Principles of Model Checking
   • Optional:
     (1) The temporal logic of programs
     (2) Design and synthesis of synchronization skeletons using branching-time temporal logic
     (3) Specification and verification of concurrent systems in CESAR
9. 07-19, 13:30:16:00, 1A-502: Symbolic Model Checking with BDDs (by Yedi Zhang)
   • Mandatory:
     (1) Slides from EECS 219C of Berkeley
   • Optional:
     (1) Symbolic model checking: 10^20 states and beyond
     (2) Symbolic Model Checking for Sequential Circuit Verification
     (3) Slides from CS357 of Stanford
10. 07-20, 13:30:16:00, 1A-402: Static analysis: dataflow analysis (by Feng Wang)
    • Mandatory:
      (1) Part 6 of Lecture Notes on Static Analysis
    • Optional:
      (1) Lecture 2 of CS 252r@Harvard
      (2) Chapter 9.2 and 9.3 of Compilers: Principles, Techniques and Tools
11. 07-21, 13:30:16:00, 1A-502: Static analysis: abstract interpretation (by Jun Zhang)
    • Mandatory:
      (1) Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
      (2) Abstract Interpretation
    • Optional:
      (1) Abstract Interpretation Frameworks
      (2) stanford CS357 Lecture16
      (3) Chapter 4 of Principles of Program Analysis
12. 07-24, 13:30:16:00, 1A-502: Static analysis: interprocedural analysis (by Pengfei Gao)
    • Mandatory:
      (1) Chapter 12 of Compilers: Principles, Techniques and Tools
    • Optional:
      (1) Chapter 2.5 of Principles of Program Analysis
      (2) Program Analysis via Graph Reachability
13. 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
14. 07-26, 13:30:16:00, 1A-402: Symbolic Model Checking with SAT/SMT (by Fu Song)
    • [Slides]
    • Mandatory:
      (1) Bounded Model Checking
    • Optional:
      (1) Slides from CS357 of Stanford
      (2) LTL Bounded Model Checking
      (3) Bounded model checking of software using SMT solvers instead of SAT solvers
      (4) Symbolic Model Checking without BDD
      (5) Linear Encodinges of Bounded LTL Model Checking
      (6) CBMC
15. 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
16. 07-28, 13:30:16:00, 1A-502: Protocol Model Checking (by Yao Zeng)
    • Mandatory:
      (1) Model Checking: A Tutorial Overview
    • Optional:
      (1) Model Checking for Security Protocols
      (2) Model Checking Security Protocols
      (3) An attack on the Needham-Schroeder public-key authentication protocol

Note: schedule is subject to change.

Books

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