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:
- Learn to create mathematical models of cyberphysical systems
- Learn the fundamental principles of verification
- Gain experience in using powerful verification tools (model checkers, SMT solvers, theorem provers, and neural network verifiers)
- Read and discuss recent ideas from research papers
- 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 (ML) and AI enabled systems.
Instructor: Prof. Huan Zhang (huanz at illinois dot edu)
Teaching assistant: Keyi Shen (keyis2 at illinois dot edu)
Canvas (for homework submission): https://canvas.illinois.edu/courses/56512
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 are available from here.

Lectures
Time: Tuesday and Thursday 11:00AM – 12:20PM
Location: 3015 Electrical & Computer Eng Bldg (ECEB)
Zoom (for UIUC online MS Eng students only): https://illinois.zoom.us/j/89423827505?pwd=yszhKhjHU4985RTNUze0N1DkJ0KNjL.1 (Passcode: 818094)
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: 10%
- Midterm presentation: 10%
- Final presentation (EOS): 15%
- Report (EOS), code and documentation: 20%
- Participation: 5%
- Provide feedback on peer projects
- Class participation, new problem suggestions and solutions
Important Dates:
- Project Proposal due: March 3
- Midterm presentation (5 mins): Week after Spring break
- 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, the TA and the instructor will provide weekly office hours (both in person and Zoom options available).
TA Office Hours: Tuesdays 3:30 – 4:30 pm Central Time (ECEB 3034 or Zoom). Please book your appointment 24 hours in advance: in-person or zoom. For your appointment, you will be asked to provide a brief description of your questions.
Instructor Office Hours: Thursdays 3:30 – 4 pm Central Time (CSL 262; Zoom is possible). Before you come to my office hour, please book your appointment 24 hours in advance here (two 15-min slots available). After booking, you should receive a confirmation email (if not, please check your spam folder). Additional office hours are available upon request.
No office hours are held during Spring break or holidays. The office hours are available for officially registered students only. If you are auditing, please email the instructor/TA to book a meeting instead since we may not have the capacity to handle your question.