Rose Bohrer
Rose

Rose Bohrer,
Assistant Professor of Computer Science

Rose is an interdisciplinary researcher whose interests range from formal methods and programming language foundations to human-computer interaction, trans studies, and computational media studies. Her thesis work focused on the verification of safety-critical cyber-physical systems (CPSs), meaning any system where a computer controls a physical device. She used programming languages to model the physical and cyber parts of a CPS, then uses theorem-proving to decide what correctness means and rigorously show that a system is correct. More recent works range from session types to trans game studies.

Graduate Students: I have finished hiring my initial PhD students and am not recruiting graduate students at this time.

Current PhD Students

  • Kaveh Eskandari Miandoab (CS, Since 2022)
  • Shano Liang (Computational Media, Since 2022)
  • Yichi Xu (CS, Since 2023)

To learn more about my research, see recent publications below. Learn more about my teaching on the teaching page.

Selected Research

Constructive Game Logic

Kaisar Proof Language

Verified Execution Pipeline

KeYmaera X Verification

Hybrid Logic for Hybrid Information Flow

CoasterX: Roller Coaster Verification

Textbooks

Rose Bohrer.
Human-Centered Programming Languages.
2023. Self-published. © The author.
book

Theses

Rose Bohrer.
Practical End-to-End Verification of Cyber-Physical Systems.
May 2021. CMU PhD Thesis. © The author.
thesis slides proposal

Rose Bohrer
Certifying Compilation for Logic Programs.
CMU SCS Undergrad Honors Thesis, 2014.
Available upon request. The VSTTE paper is recommended instead.

Refereed Conference+Workshop Publications

Rose Bohrer.
Centering Humans in the Programming Languages Classroom: Building a Text for the Next Generation
SPLASH-E Symposium
SPLASH-E 2023, Cascais, Portugal, October 25, 2023. © The author.
pdf

Shano Liang, Michelle V. Cormier, Phoebe Toups Dugas, and Rose Bohrer.
ACM Symposium on Computer-Human Interaction in Play
CHI PLAY 2023, Stratford, Canada, October 10-13, 2023. © The authors.
pdf

Charlotte Clark and Rose Bohrer.
Homotopy Type Theory for Sewn Quilts
ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design
FARM 2023, Seattle, USA, September 8, 2023. © The authors.
pdf

Rose Bohrer.
Chemical Case Studies in KeYmaera X
27th International Conference on Formal Methods for Industrial Critical Systems
FMICS 2022, Warsaw, Poland, September 14-15, 2022, Spring, 2022. © The author.
pdf

Rose Bohrer and André Platzer.
Refining Constructive Hybrid Games
5th International Conference on Formal Structures for Computation and Deduction
FSCD 2020, Natal, Brazil, June 29-July 6, 2020, LIPIcs, 2020. © The authors.
pdf

Rose Bohrer and André Platzer.
Constructive Hybrid Games
10th International Joint Conference on Automated Reasoning
IJCAR 2020, Paris, France, June 29-July 5, 2020, Springer, 2020. © The authors.
pdf

Rose Bohrer, and André Platzer.
Constructive Game Logic
29th European Symposium on Programming
ESOP 2020, Dublin, Ireland, 2020, Springer, 2020. © The authors.
pdf

Rose Bohrer, Manual Fernandez, and André Platzer.
dLɩ: Definite Descriptions in Differential Dynamic Logic
27th International Conference on Automated Deduction
CADE 2019, Natal, Brazil, August 27-30, 2019, Springer, 2019. © Springer.
pdf

Rose Bohrer, Karl Crary.
TWAM: A Certifying Abstract Machine for Logic Programs
Verified Software. Theories, Tools, and Experiments - 10th International Conference
VSTTE 2018, Oxford, UK, July 18-19, 2018, Springer, 2018. © Springer.
pdf report on arXiv Undergrad thesis available upon request.

Rose Bohrer and André Platzer.
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow.
Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science,
LICS 2018, Oxford, UK, July 9-12, 2018, ACM, 2018. © The authors.
pdf

Rose Bohrer, Adriel Luo, Xuean Chuang, and André Platzer.
CoasterX: A Case-Study in Component-Driven Hybrid Systems Proof Automation.
IFAC Conference on Analysis and Design of Hybrid Systems,
ADHS 2018, Oxford, UK, July 11-13, 2018, IFAC, 2018. © IFAC.
pdf | extended slides

Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer.
VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models.
Programming Language Design and Implementation - 39th ACM SIGPLAN Conference,
PLDI 2018, Philadelpha, PA, June 18-22, 2018, ACM, 2018. © The authors.
pdf Isabelle/HOL

Nathan Fulton, Stefan Mitsch, Rose Bohrer, and André Platzer.
Bellerophon: Tactical Theorem Proving for Hybrid Systems.
8th International Conference on Interactive Theorem Proving,
ITP 2017, Brasilia, Brazil, September 26-29, ACM, 2017. © ACM.
pdf

Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer.
Formally verified differential dynamic logic.
Certified Programs and Proofs - 6th ACM SIGPLAN Conference,
CPP 2017, Paris, France, January 16-17, 2017, ACM, 2017. © ACM
pdf Isabelle/HOL

Journal Publications

Ichiro Hasuo, Clovis Eberhart, James Haydon, Jeremy Dubut, Rose Bohrer, Tsutomu Kobayashi, Sasinee Pruekprasert, Xiao-Yi Zhang, Erik Andre Pallas, Akihisa Yamada, Kohei Suenaga, Fuyuki Ishikawa, Kenji Kamijo, Yoshiyuki Shinya, and Takamasa Suetomi.
Goal-Aware RSS for Complex Scenarios via Program Logic.
Transactions on Intelligent Vehicles
IEEE IV, 2022, IEEE, 2022. © IEEE.
pdf

Rose Bohrer and Bashima Islam.
Cyber-Physical Verification of Intermittently-Powered Embedded Systems.
22nd International Conference on Embedded Software
EMSOFT 2022, Shanghai, October 10-15, 2022, IEEE, 2022. © The authors.
ACM TCAD. pdf

Rose Bohrer and André Platzer.
Structured Proofs for Adversarial Cyber-Physical Systems
21st International Conference on Embedded Software
EMSOFT 2021, The Internet, October 10-15, 2021, IEEE, 2021. © The authors.
ACM TECS. pdf

Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, and André Platzer.
A Formal Safety Net for Waypoint-Following in Ground Robots.
IEEE Robotics Automation Letters. 4(3), IEEE, 2019. © IEEE.
pdf

Non-Refereed Publications

Rose Bohrer.
Imagining Introductory Rust
RustEdu Workshop
RustEdu 2022, Virtual, 2022. © The author.
pdf