Skip to content


Refereed Journal Publications

Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer.
How to model and prove hybrid systems with KeYmaera: A tutorial on safety. Software Tools for Technology Transfer (STTT). 2015. (10.1007/s10009-015-0367-0pdf, videos)

Refereed Conference Publications

Sarah M. Loos and André Platzer.
Differential Refinement Logic
In ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York City, USA, July 5–8, 2016. (pdf)

Sarah M. Loos, David Witmer, Peter Steenkiste, and André Platzer.
Efficiency Analysis of Formally Verified Adaptive Cruise Controllers.
In 16th International IEEE Conference on Intelligent Transportation Systems, ITSC 2013, The Hague, The Netherlands, Proceedings, 2013. (10.1109/itsc.2013.6728453pdf, slides)

Sarah M. Loos, David Renshaw, and André Platzer.
Formal Verification of Distributed Aircraft Controllers (Case study paper).
In Hybrid Systems: Computation and Control, HSCC, Philadelphia, USA, April 8-11. 2013.
(10.1145/2461328.2461350pdf, slides, poster)

Nikos Aréchiga, Sarah M. Loos, André Platzer, and Bruce H. Krogh.
Using theorem provers to guarantee closed-loop system properties.
In Dawn Tilbury, editor, American Control Conference, ACC, Montréal, Canada, June 27-29. 2012.

Stefan Mitsch, Sarah M. Loos, and André Platzer.
Towards Formal Verification of Freeway Traffic Control.
In International Conference on Cyber-Physical Systems, ICCPS, Beijing, China, April 17-19. 2012.(10.1109/iccps.2012.25pdfslides)

Akshay Rajhans, Ajinkya Bhave, Sarah M. Loos, Bruce H. Krogh, André Platzer, and David Garlan.
Using parameters in architectural views to support heterogeneous design and verification.
50th IEEE Conference on Decision and Control and European Control Conference, CDC, Orlando, USA. 2011. (10.1109/cdc.2011.6161408pdf)

Sarah M. Loos and André Platzer.
Safe Intersections: At the Crossing of Hybrid Systems and Verification.
In 14th International IEEE Conference on Intelligent Transportation Systems, ITSC 2011, Washington, D.C., USA, Proceedings, 2011. (10.1109/itsc.2011.6083138pdfslides)

David Renshaw, Sarah M. Loos, and André Platzer.
Distributed theorem proving for distributed hybrid systems.
In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM’11, Durham, United Kingdom, ProceedingsLNCS. Springer, 2011. (10.1007/978-3-642-24559-6_25pdf)

Sarah M. Loos, André Platzer, and Ligia Nistor.
Adaptive cruise control: Hybrid, distributed, and now formally verified.
In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, ProceedingsLNCS. Springer, 2011. (10.1007/978-3-642-21437-0_6pdfslides)

Sarah M. Loos and David S. Wise.
Strassen’s Matrix Multiplication Relabeled.
ACM Student Research Competition, December 2009. (link)


Sarah M. Loos.
[THESIS] Differential Refinement Logic. September 2015.
School of Computer Science, Carnegie Mellon University, CMU-CS-15-144, 2015. (pdf, slides)

Sarah M. Loos.
[THESIS PROPOSAL] Differential Refinement Logic. December 2014.(pdf, slides)


Sarah M. Loos and André Platzer.
[DRAFT] Teaching Cyber-Physical Systems with Logic. October 2014. (pdf)