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 checkers, SMT 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 systems, by 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

• Homework (4 sets): 40%
  • Problems will involve some coding and pencil paper proofs
• Project: 55%
  • Proposal: 5%
  • Midterm presentation: 5%
  • Final presentation (EOS): 20% 
  • Report (EOS): 20% 
  • Code and documentation: 5%
• Participation: 5%
  • Class participation
  • Feedback on projects
  • New problem suggestions and solutions

Important Dates:

• Project Proposal: Feb 23 March 3
• Midterm presentation (5 mins): Week after Spring break March 26 & 28 (slides uploaded to Canvas by March 25)
• Final presentations: Last week of instruction
• Final report: Due final’s week

Homework

There will be 4 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 

• You will work on a semester-long research project building a verification system. Often the projects become publishable.
• Good project will require ~6-8 hours/week — higher towards the end of the semester.  
• Start early, and get frequent feedback.
• Projects can either be individual or be done in a team of 2 people. If you are sure that you want to work in a larger team (3 or more people), you can make a case and we can consider. 
• Projects will be graded based on
  • soundness of claims, 
  • significance (novelty, impact, harness), 
  • presentation quality, and 
  • effort
• Advice
  • Choose a high-risk project that if success will make you proud
  • Clearly define the problem ASAP
  • Get feedback frequently

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). The office hours are available for officially registered students only. If you are auditing, please email the instructor to book a meeting instead.