ECE/CS 584: Spring 2024

Verification of embedded and cyberphysical systems

Verification is the art and science of establishing that a given system meets a given set of requirements. For example, an assertion such as “an adaptive cruise control system in a car does not lead to any collisions.” 

Cyberphysical systems (CPS) combine software components with sensors, actuators & communication. From driverless cars to air-traffic control systems, medical devices to manufacturing robots, many new and old engineering systems fit the description of what are now called cyberphysical systems.

Many CPS systems are mission-critical, so verification is essential for their applications. In particular, the use of machine learning and AI in these systems will make the verification of these systems even more challenging.

In this course, you will:

  1. Learn to create mathematical models of cyberphysical systems
  2. Learn the fundamental principles of verification
  3. Gain experience in using powerful verification tools (model checkersSMT solvers, theorem provers, and neural network verifiers
  4. Read and discuss recent ideas from research papers
  5. Gain in experience in formulating research problems in the area of cyberphysical systems/formal verification. This course especially highlights the recent developments in the formal verification of machine-learning-enabled systems.

Instructor: Prof. Huan Zhang (huanz at illinois dot edu)
Office: CSL 262
Canvas (for homework submission): https://canvas.illinois.edu/courses/44138

Book

The course will largely follow the textbook by Prof. Sayan Mitra, with additional components on the verification of machine learning enabled systems. Additional readings may be assigned before each lecture.

Verifying cyberphysical systemsby Sayan Mitra, published by MIT Press, 2021. Supplementary materials available from here.

Lectures

Time: Tuesday and Thursday 11:00AM – 12:20PM
Location: 3015 Electrical & Computer Eng Bldg
Zoom (for UIUC online MS Eng students only): https://illinois.zoom.us/j/85883565343?pwd=djFYTTdWbnAyKzRvZkd2TVdtblordz09 (Passcode: 611033)

You will be required to do the assigned reading from the above book draft ahead of time. The lectures will not repeat the same topics but provide a complementary view of the material in the book. 

Grading

Important Dates:

Homework

There will be 4-5 sets of individual homework. The homework problems will involve pencil-paper proofs and some coding. The homework will be concentrated on the earlier 2/3rd of the semester.

Homework submission: homework needs to be submitted on Canvas. Submissions through other channels will not be accepted. Homework will be due at 11:59 pm CT on the due date.

Late policy: for each late day, there will be a 20% penalty on your grade. After 5 days, late homework will not be accepted. For example, if you submitted your homework two days late and scored 90, your grade for this late homework will be 90*60%=54. For medical excuses, please email me your absence letter from the Office of the Dean of Students.

Course Project 

Office hours

Each week, I have 1 hour of in-person office hours (CSL 262) and 1 hour of online office hours (Zoom) available upon appointment, except for the Spring break (March 9 – 17) and holidays. Each hour will be split into three 20-minute slots. Before you come to my office hour, please book your appointment 24 hours in advance: in-person or virtual. After booking you should receive a confirmation email (if not, please check your spam folder).