Brandon Bohrer,
PhD Student in Computer Science

I am a fourth-year PhD student advised by André Platzer working in the Logical Systems Lab. We look at the verification of safety-critical cyber-physical systems (CPS). As my project list shows, I like to keep a wide range of research interests, but a common theme is pushing CPS verification further toward practical use while maintaining rigor. For example my work looks at improving scalability for both automatic and interactive proofs, while also considering underexplored practical domains (roller coasters, smart grids). At the same time my work also looks at maintaining the highest level of rigor, such as by verified a proof checker for CPS proofs and integrating it into a verified pipeline for the generation and compilation of safe controllers.

Check out my research projects below, or jump straight to my publications, or my teaching.

My awards include the NDSEG Fellowship, NSFGRFP Honorable Mention, and the CMU Scool of Computer Science's Alan Perlis Graduate Teaching Award.

My Research

Hybrid Logic for Hybrid Systems Information Flow

CoasterX: Roller Coaster Verification

Verified Execution Pipeline

KeYmaera X Verification

Kaisar Proof Language

Certifying Compiler for Prolog

Refereed Conference Publications

Brandon 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.
To appear. preprint

Brandon 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.

Brandon 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.

Brandon 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

Brandon 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.

Nathan Fulton, Stefan Mitsch, Brandon 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.

Brandon 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

Miscellaneous Publications

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, and André Platzer.
Blackbox End-to-End Verification of Ground Robot Safety and Liveness
arXiv preprint

Brandon Bohrer and André Platzer.
Kaisar: Structured Proofs for Dynamic Logics.
Draft. Available upon request.

Brandon Bohrer and Karl Crary.
TWAM: A Certifying Abstract Machine for Logic Programs.
In submission.
arXiv preprint

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