Please refer to Canvas for the latest information.
The course code and title were MICS6000A Automated Reasoning for Electronic System Verification in Spring 2022.
- 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
We will try to follow the posted schedule below.
||Introduction, Propositional Logic
||Survey of hardware and software vulnerabilities
||SAT solver: extensions and applications
||Symbolic model checking
||SAT-based model checking
||SAT application: logic equivalence checking
||Use of model checkers (TA tutorial session)
||Neural network verification
||Abstraction in verification, security verification
||Final Project Presentation
- Participation in seminars : 20%
- Problem sets : 30%
- Projects : 30%
- Final exam : 20%
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.
- 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
- Survey of Approaches for Security Verification of Hardware/Software Systems Link