MICS5510 Formal Methods and Testing for Electronic System Verification


Date
Sep 4, 2024 1:30 PM — Dec 4, 2024 4:20 PM
Location
E4-201

Please refer to Canvas for the latest information.

The course code and title were MICS6000A Automated Reasoning for Electronic System Verification in Spring 2022.

Logistics

  • Lecture: Wednesday, 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

We will follow the posted schedule below.

Week Date Lecture Seminar
1 Sep 4 Introduction, Propositional Logic
2 Sep 11 First-Order Logic Survey of hardware and software vulnerabilities
3 Sep 18 SAT solvers
4 Sep 25 SMT solvers SAT solver: extensions and applications
5 Oct 9 Temporal Logic
6 Oct 16 Symbolic model checking
7 Oct 23 SAT-based model checking
8 Oct 30 Hoare Logic SAT application: logic equivalence checking
9 Nov 6 Abstraction Use of model checkers (TA tutorial session)
10 Nov 13 Testing (pre-silicon) Neural network verification
11 Nov 20 Testing (post-silicon) Abstraction in verification, security verification
12 Nov 27 Syntax-Guided Synthesis
13 Dec 4 Course Summary 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

  • 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
Hongce Zhang
Hongce Zhang
Assistant Professor in Microelectronics Thrust

My research interest is on hardware formal verification.