Problem Sets



People Involved

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

Spring 2016

ECE/CS 584: Embedded & Cyberphysical System Verification


Date Topic Notes Reading
L1 Tue 01/19 Motivation. Modeling Discrete Systems. Automata. HIOA Language. Invariants. slides (.pdf) Decidability & Complexity from [MSip96]
L2 Thu 01/21 Turing Machines, Languages and Decidability slides (.pdf)
L3 Tue 01/26 Complexity classes, P, NP, NL, PSPACE. NL Completeness of Reachability. slides (.pdf)
L4 Thu 01/28 Symbolic Reachability. Fix point characterization. slides (.pdf)
Chapter 3 [CGP00]
L5 Tue 02/02 An introduction to modern SMT solvers. Z3 tutorial.
slides (.pdf) References in slides
L6 Thu 02/04 Z3 tutorial continued

slides (.pdf)
Z3 files (.zip)

Read [TIOA06] Chapters 1-3
L7 Tue 02/09 Hybrid automata. Executions, Examples.
slides (.pdf) Read [TIOA06] Chapters 1-3
L8 Thu 02/11 Reachability. Examples.
slides (.pdf)
L9 Tue 02/16

Executions, reachability, inductive invariants

slides (.pdf)
L10 Thu 02/18 Compositions, abstractions and Simulation slides (.pdf)
L11 Tue 02/23 PVS Tutorial: Intro

slides (.pdf)

PVS website
L12 Thu 02/25 PVS Tutorial: Language slides (.pdf) Stacks, MinProblem, TokenRing theories
L13 Tue 03/01

PVS Tutorial: Prover

slides (.pdf)
L14 Thu 03/03 Abstraction and simulation relations; weak, strong, time-abstract

slides (.pdf)

Read [AD 94]
L15 Tue 03/08 Timed automata Automata;
slides (.pdf)  
L16 Thu 03/10 Timed to to rectangular hybrid automata slides (.pdf) [Henz95]
Tue 03/15 No class SpaceEx website
Thu 03/17 Project review
  Tue 03/22-24 Spring break
L17 Tue 03/29 Undecidable problems for timed and hybrid automata slides (.pdf)
Thu 03/31 Stability verification, dynamical systems, Lyapunov functions slides (.pdf)
Tue 04/05 Stability verification, hybrid systems, Multiple Lyapunov functions, dwell time slides (.pdf)
Thu 04/07 Temporal logic and controller synthesis slides (.pdf)
  04/12-14 No class    
Tue 04/19 Simulation-based verification: C2E2 Tutorial 1 Guest lecture by Chuchu Fan
L22 Thu 04/21

TBA: Guest Lecture by James Lenz and Ashley Greer

L23 Tue 04/26 C2E2 Tutorial 2

P1 Thu 04/28 Project presentations 1,2,3    
P2 May 05/03 Project presentations 4,5,6

Project presentations