Brandon

Brandon Bohrer,
PhD Student in Computer Science

I am a fifth-year PhD candidate advised by André Platzer working in the Logical Systems Lab. We look at the verification of safety-critical cyber-physical systems (CPS). My research seeks to provide novel rigorous foundations for CPS verification which enable verification of practical systems. My current focus is the constructive logic of hybrid games and its applications to synthesis. This builds on my prior work verifying a proof checker for CPS proofs and integrating it into a verified pipeline for the generation and compilation of safe controllers. I also look at improving scalability for both automatic and interactive proofs, while also considering underexplored practical domains (roller coasters, smart grids).

My research is described in my thesis proposal and below, also see my teaching.

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

I plan to be on the market for academic jobs in Fall 2020

Selected Research


Constructive Game Logic

Kaisar Proof Language

Verified Execution Pipeline

KeYmaera X Verification

Hybrid Logic for Hybrid Information Flow

CoasterX: Roller Coaster Verification

Refereed Conference Publications


Brandon 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, 2012, LIPIcs, 2020. © The authors.
To appear. preprint

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

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

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

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.
pdf report on arXiv Bachelor's thesis available upon request.

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

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.
pdf Isabelle/HOL

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

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
pdf Isabelle/HOL

Journal Publications


Brandon 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 arXiv preprint

Proposals


Brandon Bohrer.
Practical End-to-End Verification of Cyber-Physical Systems.
October 2019. CMU. © The author.
thesis proposal

Brandon Bohrer and André Platzer.
Toward Structured Proofs for Dynamic Logics arXiv, proposed design