Brandon Bohrer,
PhD Student in Computer Science

My name is Brandon, and I want to save the world with proofs. I am a third-year PhD student advised by André Platzer working in the Logical Systems Lab. More specifically, my interests include formally verifying critical systems such as compilers and proof assistants and developing new languages and tools to make theorem-proving easier. I like doing all this in the context of cyber-physical systems (CPS) because CPSs are some of the most safety-critical systems in the world. I use Isabelle/HOL for a lot of my proofs.

Check out my research projects below, or jump straight to my publications, but don't forget to check out my teaching as well.

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

My Research

KeYmaera X Verification

KeYmaera X Development

Kaisar Proof Language

Verified Execution

ACAS X Verification

Certifying Compiler for Prolog


Nathan Fulton, Stefan Mitsch, Brandon Bohrer, and André Platzer.
Bellerophon: Tactical Theorem Proving for Hybrid Systems.
Interactive Theorem Proving (ITP) 2017.

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

Brandon Bohrer
Certifying Compilation for Logic Programs.
CMU SCS Honors Thesis, 2014.