Logistics
-
Lecture: Online, Monday, Wednesday 10:30 AM-11:50 AM
-
Instructor: Hongce Zhang (e-mail: hongcezh AT ust DOT hk)
-
Office Hours: Friday 3-4:30 pm (please e-mail me in advance and I will send you the Zoom link)
Schedule (Tentative)
We will try to follow the posted schedule below. However, as it is the first time I teach this course, changes are likely.
Week |
Date |
Lecture |
Seminar |
1 |
Feb 7, Feb 9 |
Introduction, Propositional Logic |
|
2 |
Feb 14, Feb 16 |
First Order Logic |
Survey of hardware and software vulnerabilities |
3 |
Feb 21, Feb 23 |
SAT solvers |
|
4 |
Feb 28, Mar 2 |
SMT solvers |
SAT solver: extensions and applications |
5 |
Mar 7, Mar 9 |
Temporal Logic |
SMT solver: Nelson-Oppen |
6 |
Mar 14, Mar 16 |
Symbolic model checking |
|
7 |
Mar 21, Mar 23 |
SAT-based model checking |
|
8 |
Mar 28, Mar 30 |
Hoare Logic |
SAT application: logic equivalence checking |
9 |
Apr 4, Apr 6 |
Predicate abstraction |
Model checking applications (TA tutorial session) |
10 |
Apr 11 |
Abstraction and Refinement |
|
11 |
Apr 20 |
|
Hot topic: neural network verification |
12 |
Apr 25, Apr 27 |
Concolic testing, Syntax-Guided Synthesis |
|
13 |
May 4 |
|
Abstraction in verification, security verification |
14 |
May 11 |
|
Final project presentation |
Grading
- Participation in seminars : 20%
- Problem sets : 30%
- Projects : 30%
- Final exam : 20%
Resources
-
Textbook: The Calculus of Computation: Decision Procedures with Applications to Verification (by Aaron R. Bradley and Zohar Manna). Electronic version.
We will use the “Foundations” part of the book.
-
Reference book: Handbook of Model Checking. Electronic version. This book serves as a good supplement on the algorithmic discussion.
-
Reference papers:
- SAT: Joao Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability, Chapter 4, 2008.
- SMT: Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9, 2011.
- BDD: Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 100 (8), 677-691, 1986.
- Temporal Logic and BDD-based Model Checking: E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8, 2 (April 1986), 244-263.
- BMC: Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu. Symbolic Model Checking without BDDs. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS) Conference 1999: 193-207.
- PDR: Niklas Een, Alan Mishchenko, Robert Brayton. Efficient Implementation of Property Directed
Reachability. In Proceedings of Formal Methods in Computer-Aided Verification (FMCAD) Conference 2011: 125-134.
- Hoare Logic: C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12, 10, 576-580, 1969.
- Software Model Checking: Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Computing Surveys 41, 4, Article 21, 2009.
- SyGuS: Rajeev Alur, Rastislav Bodík, and others. Syntax-guided synthesis. In Proceedings of FMCAD 2013: 1-8.
Readings suggested for seminars
Below are simply suggestions. You may pick your favourite instead.
-
Survey of hardware and software vulnerabilities
- Binary Exploitation - Buffer Overflow Explained in Detail Link
- Survey of Transient Execution Attacks and Their Mitigations Link
-
SAT solver: extensions and applications
- A comparison of encodings for cardinality constraints in a SAT solver. Link
-
SMT solver: Nelson-Oppen
-
SAT application: logic equivalence checking
- Improvements to Combinational Equivalence Checking Link
-
Model checking applications (TA will give the tutorial)
-
Hot topic: neural network verification
- Towards Proving the Adversarial Robustness of Deep Neural Networks Link
-
Abstraction in verification
- Abstraction Mechanisms for Hardware Verification Link
-
Security verification
- Survey of Approaches for Security Verification of Hardware/Software Systems Link