Home

Administrivia

Project Jumpstart

Schedule

Problem Sets

Resources

Archives
2025

Sayan Mitra
Lecturer
mitras at illinois.edu
Phone: 333-7824
Office: CSL 266

Fall 2025

ECE/CS 584: Embedded & Cyberphysical System Verification

Course Administrivia

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.

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.

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

Lectures

Time: Tuesday and Thursday 12:30PM – 1:50PM
Location: 3013 Electrical & Computer Eng Bldg

Zoom link: link (Meeting id: 876 6537 3411, Passcode: 585899)

Teaching Assistant: Chenxi Ji (email: chenxij2 at illinois.edu)
Office Hours: Thursdays 11am-noon, ECEB 3003

Lecture Recordings: Mediaspace channel

Campuswire: Link for occasional announcements and discussions. If you registered for the class then you should have received an email invitation to join.

Grading

• Homework (4-5 sets): 40%
  • Problems will involve some coding and pencil paper proofs
• One Midterm: 15%
  • In class pencil paper problems
• Project (Group of 1 or 2): 40%
  • Proposal: 5%
  • Midterm presentation: 5%
  • Final presentation (EOS): 15%
  • Report (EOS): 10%
  • Code and documentation: 5%
• Participation: 5%
  • Feedback on projects
  • Class participation
  • New problem suggestions and solutions

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 Gradescope. 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

Prof. Mitra: Tuesdays 2-3pm, CSL 266

Chenxi Ji: Thursdays 11am-noon, ECEB 3003