16 citations · 29 across the 8 of their papers we have counts for
8 papers
Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
Radu-Florin Tulcan, Rose Bohrer, Yoàv Montacute +3
We introduce a hybrid spatiotemporal logic for automotive safety applications (HSTL), focused on highway driving. Spatiotemporal logic features specifications about vehicles throug…
Goal-Aware RSS for Complex Scenarios via Program Logic
Ichiro Hasuo, Clovis Eberhart, James Haydon +12
We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS r…
Chemical Case Studies in KeYmaera X
Rose Bohrer
Safety-critical chemical processes are the backbone of multi-billion-dollar industries, thus society deserves the strongest possible guarantees that they are safe. To that end, mod…
Refining Constructive Hybrid Games
Rose Bohrer, André Platzer
We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. We use this connective to prove a folk theorem…
Constructive Hybrid Games
Rose Bohrer, André Platzer
Hybrid games are models which combine discrete, continuous, and adversarial dynamics. Game logic enables proving (classical) existence of winning strategies. We introduce construct…
Constructive Game Logic
Rose Bohrer, André Platzer
Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective…
Toward Structured Proofs for Dynamic Logics
Rose Bohrer, André Platzer
We present Kaisar, a structured interactive proof language for differential dynamic logic (dL), for safety-critical cyber-physical systems (CPS). The defining feature of Kaisar is…
TWAM: A Certifying Abstract Machine for Logic Programs
Rose Bohrer, Karl Crary
Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a type-preserving compiler for a s…