| Date |
Topic |
Readings |
Slides/Summaries |
Lead |
| 8/21 |
Course Introduction, General Introduction |
-- |
Course Intro, CPS Verification Intro |
Jyo |
| 8/28 |
Software Verification |
A1. Ranjit Jhala, Rupak Majumdar: Software model checking. ACM Comput. Surv. 41(4): 21:1-21:54 (2009) |
A1 summary |
P: Anand, Zunchen S: Xin, Minyang |
| 9/4 |
Invited Talk by Yash Vardhan Pant from UPenn |
-- |
Talk summary ** |
-- |
| 9/11 |
Hybrid Systems Reachability |
A2. X. Chen, E. Abraham, S. Sankaranarayanan: Taylor model Flowpipe Construction for Non-linear Hybrid Systems. In IEEE Real-Time Systems Symposium, 2012.
A3. C. Le Guernic, A. Girard, Reachability analysis of hybrid systems using support functions. In International Conference on Computer Aided Verification, 2009. |
A2, A3 summary |
P: Sara, Jingbo, S: Chungha, Brandon |
| 9/18 |
Verification Beyond Reachability |
A4. A. Donzé, O. Maler, Systematic simulation using sensitivity analysis. In Hybrid Systems: Computation and Control, 207.
A5. S. Prajna, A. Jadbabaie, Safety verification of hybrid systems using barrier certificates. In Hybrid Systems: Computation and Control, 2004.
A6. S. Gao, S. Kong, E. M. Clarke, Satisfiability modulo ODEs. In Formal Methods in Computer-Aided Design (FMCAD), 2013 |
A4, A5, A6 summary |
TBD |
| 9/25 |
Introduction to Temporal Logic |
Temporal Logic |
-- |
TBD |
| 10/2 |
Temporal Logic Robustness |
B2. G. Fainekos, G. Pappas, Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 2009
B3. S. Jaksic, E. Bartocci, R. Grosu, D. Nickovic, Quantitative monitoring of STL with edit distance. In International Conference on Runtime Verification (pp. 201-218) | B2, B3 summary |
TBD |
| 10/9 |
No class: ATVA conference |
-- |
-- |
Jyo |
| 10/16 |
Proposal Presentations |
-- |
-- |
TBD |
| 10/23 |
Misc. Topics |
B1. J. Kapinski, J. Deshmukh, X. Jin, H. Ito, K. Butts, Simulation-based Approaches for Verification of Embedded Control Systems, IEEE Control Systems, 36(6), 45-64, 2016.
B4. T. Wongpiromsarn, U. Topcu, and A. Lamperski, Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems, IEEE Transactions on Automatic Control 2016. |
B1, B4 summary |
TBD |
| 10/30 |
Stochastic Verification |
B5. M. Kwiatkowska, G. Norman, and D. Parker, Stochastic model checking, International School on Formal Methods for the Design of Computer, Communication and Software Systems |
B5 summary |
TBD |
| 11/6 |
CPS security |
C0. F. Pasqualetti, F. Dorfler, and F. Bullo, Control-theoretic methods for cyberphysical security: Geometric principles for optimal cross-layer resilient control systems, IEEE Control Systems, 2015 |
C0 summary |
TBD |
| 11/13 |
AI verification/safety |
C1. G. Katz, C. Barrett, D. Dill, K. Julian, M. Kochenderfer, Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification 2017.
C2. M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, U. Topcu, Safe reinforcement learning via shielding, AAAI 2017. |
C1, C2 summary |
TBD |
| 11/20 |
AI verification/testing |
C3. S. Ghosh, F. Berkenkamp, G. Ranade, S. Qadeer, S., A. Kapoor, Verifying Controllers Against Adversarial Examples with Bayesian Optimization, ICRA 2018.
C4. C. E. Tuncali, G. Fainekos, H. Ito, J. Kapinski, Simulation-based Adversarial Test Generation for Autonomous Vehicles with Machine Learning Components, Intelligent Vehicles Symposium 2018 |
C3, C4 summary |
TBD |
| 11/27 |
Final Project Presentations |
-- |
-- |
Jyo |