The course code and title were MICS6000A Automated Reasoning for Electronic System Verification in Spring 2022.
Logistics
- Lecture: mixed-mode, Tuesday, 13:30 PM-16:20 PM
- Instructor: Hongce Zhang (e-mail: hongcezh AT ust DOT hk)
- Office Hours: Friday 4:00-6:00 pm
Schedule (Tentative)
We will try to follow the posted schedule below.
Week |
Date |
Lecture |
Seminar |
1 |
Feb 7 |
Introduction, Propositional Logic |
|
2 |
Feb 14 |
First-Order Logic |
Survey of hardware and software vulnerabilities |
3 |
Feb 21 |
SAT solvers |
|
4 |
Feb 28 |
SMT solvers |
SAT solver: extensions and applications |
5 |
Mar 7 |
Temporal Logic |
|
6 |
Mar 14 |
Symbolic model checking |
|
7 |
Mar 21 |
SAT-based model checking |
|
8 |
Mar 28 |
Hoare Logic |
SAT application: logic equivalence checking |
9 |
Apr 11 |
Abstraction |
Use of model checkers (TA tutorial session) |
10 |
Apr 18 |
Testing (pre-silicon) |
Neural network verification |
11 |
Apr 25 |
Testing (post-silicon) |
Abstraction in verification, security verification |
12 |
May 9 |
Syntax-Guided Synthesis |
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.
Suggested readings for seminars
Below are merely suggestions. You may pick your favourite paper(s) 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