My name is Brandon, and I want to save the world with proofs. I am a second-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.
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.