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.
My awards include the NDSEG Fellowship, NSFGRFP Honorable Mention, and the CMU Scool of Computer Science's Alan Perlis Graduate Teaching Award.
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
Certifying Compilation for Logic Programs.
CMU SCS Honors Thesis, 2014.