
Franz Franchetti (PI), José M. F. Moura (CoPI), Manuela Veloso (CoPI), Andre Platzer (CoPI), Soummya Kar (CoPI), David Padua (CoPI), Jeremy Johnson (CoPI), Mike Franusich (CoPI)
Systems Scientists: Tze Meng Low
PostDocs: Stefan Mitsch, Khalil Ghorbal, JeanBaptiste Jeannin, Pooyan Fazli
PhD Students: Vadim Zaliva, Richard Veras, Yuan Chen, Liangyan Gui, Juan Pablo Mendoza, Lingchuan (LC) Meng, Amarin Phaosawasdi
Engineers: Brian Duff, Jason Larkin
Alumni: Aliaksei Sandryhaila, JanDavid Quesel, Seokje Seo, Kevin Owens, Nicolas Huynh Thien, Christos Angelopoulos


Publications
Journal Publications
Stefan Mitsch and André Platzer
ModelPlex: Verified Runtime Validation of Verified CyberPhysical System Models
Formal Methods in System Design, 49(1), pp. 3374. 2016. Special issue for selected papers from RV’14.
Stefan Mitsch, Grant Olney Passmore and André Platzer
Collaborative VerificationDriven Engineering of Hybrid Systems
8(1), pp. 7197, 2014. Special issue on Enabling Domain Experts to use Formalized Reasoning.
Stefan Mitsch, Khalil Ghorbal, Andre Platzer
On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles
Robotics: Science and Systems IX.
André Platzer
Analog and Hybrid Computation: Dynamical Systems and Programming Languages
Bulletin of the EATCS, Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
Conference Papers
Tze Meng Low and Franz Franchetti
High Assurance Code Generation for CyberPhysical Systems
Proceedings of the 18th IEEE International Symposium on High Assurance Systems Engineering (HASE 2017), Jan 2017.
Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson and André Platzer
A Method for Invariant Generation for Polynomial Continuous Systems
In Verification, Model Checking, and Abstract Interpretation, Barbara Jobstmann and K. Rustan M. Leino, Eds.
Proceedings of the17th International Conference, VMCAI 2016, St. Petersburg, Florida, USA, January 1719, 2016,
Vol. 9583 of LNCS, pp. 268288. Springer, 2016.
H. V. Koops, F. Franchetti
An Ensemble Technique for Estimating Vehicle Speed and Gear Position from Acoustic Data
Proceedings of the 20th International Conference on Digital Signal Processing (DSP) 2015, accepted.
Khalil Ghorbal, Andrew Sogokon, and André Platzer
A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets.
In Verification, Model Checking, and Abstract Interpretation, Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, Eds.
Proceedings of 16th International Conference, VMCAI 2015, Mumbai, India, January 1214, 2015, vol. 8931 of LNCS, pp. 431448. Springer, 2015.
Stefan Mitsch, André Platzer
ModelPlex: Verified Runtime Validation of Verified CyberPhysical System Models
RV 2014.
F. Franchetti, A. Sandryhaila, J. R. Johnson
High Assurance SPIRAL
Proceedings of SPIE 2014.
Stefan Mitsch, JanDavid Quesel, André Platzer
From Safety to Guilty and from Liveness to Niceness
Formal Methods for Robotics and Automation 2014.
Khalil Ghorbal and Andre Platzer
Characterizing Algebraic Invariants by Differential Radical Invariants?
TACAS 2014.
Vadim Zaliva and Franz Franchetti
Barometric and GPS Altitude Sensor Fusion
ICASSP 2014.
Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
Early Detection of Anomalous Clusters for Task Execution Monitoring
ICRA 2014.
Stefan Mitsch, JanDavid Quesel, André Platzer
Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems
FM 2014.
Stefan Mitsch and André Platzer
ModelPlex: Verified Runtime Validation of Verified CyberPhysical System Models
In Runtime Verification, Borzoo Bonakdarpour and Scott A. Smolka, Eds.
Proceedings of 5th International Conference, RV 2014, Toronto, ON, Canada, September 2225, 2014.
Vol. 8734 of LNCS, pp. 199214. Springer, 2014.
Stefan Mitsch, JanDavid Quesel and André Platzer
Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems
In Proceedings of 19th International Symposium on Formal Methods, Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, Eds.
FM, Singapore, vol. 8442 of LNCS, pp. 481496. Springer, 2014.
Khalil Ghorbal and André Platzer
Characterizing Algebraic Invariants by Differential Radical Invariants.
In Tools and Algorithms for the Construction and Analysis of Systems, Erika Ábrahám and Klaus Havelund, Eds.
Proceedings of TACAS 2014, vol. 8413 of LNCS, pp. 279294. Springer, 2014.
Khalil Ghorbal, Andrew Sogokon, and André Platzer.
Invariance of conjunctions of polynomial equalities for algebraic differential equations
In Proceeding of 21st International Static Analysis Symposium, Markus MüllerOlm and Helmut Seidl, Eds.
Vol. 8723 of LNCS, pp. 151167. Springer, 2014.
Stefan Mitsch, Grant Olney Passmore, Andre Platzer
A Vision of Collaborative VerificationDriven Engineering of Hybrid Systems
DoForm @ AISB 2013.
Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
Motion Interference Detection in Mobile Robots
IROS 2012.
Juan Pablo Mendoza, Manuela Veloso, Reid Simmons
Mobile Robot Fault Detection based on Redundant Information Statistics
IROS 2012.
