Rose Bohrer
YOU?
Author Swipe
View article: The Collaborative Sensemaking Play of Jubensha Games: A Deconstruction, Taxonomy, and Analysis
The Collaborative Sensemaking Play of Jubensha Games: A Deconstruction, Taxonomy, and Analysis Open
Jubensha games, popular in China, combine storytelling, social deduction, and script-centered group play, sparking widespread interest among gamers and researchers worldwide. However, enthusiasts and researchers have struggled to accuratel…
View article: A Coq Formalization of Unification Modulo Exclusive-Or
A Coq Formalization of Unification Modulo Exclusive-Or Open
Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, unification modulo the theory of exclusive-or. This theory co…
View article: Programming Language Case Studies Can Be Deep
Programming Language Case Studies Can Be Deep Open
In the pedagogy of programming languages, one well-known course structure is\nto tour multiple languages as a means of touring paradigms. This\ntour-of-paradigms approach has long received criticism as lacking depth,\ndistracting students …
View article: Goal-Aware RSS for Complex Scenarios via Program Logic
Goal-Aware RSS for Complex Scenarios via Program Logic Open
International audience
View article: Chemical Case Studies in KeYmaera X
Chemical Case Studies in KeYmaera X Open
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, models of chemical processes are well-studied in the formal me…
View article: Structured Proofs for Adversarial Cyber-Physical Systems
Structured Proofs for Adversarial Cyber-Physical Systems Open
Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model’s correctness specification always holds. Constructive Differential Game Logic ( CdGL ) is such a lo…
View article: Constructive Hybrid Games
Constructive Hybrid Games Open
Hybrid games combine discrete, continuous, and adversarial dynamics. Differential game logic ("Equation missing") enables proving (classical) existence of winning strategies. We introduce constructive differential game logic () for hybrid …
View article: A Formal Safety Net for Waypoint-Following in Ground Robots
A Formal Safety Net for Waypoint-Following in Ground Robots Open
We present a reusable formally verified safety net that provides end-to-end\nsafety and liveness guarantees for 2D waypoint-following of Dubins-type ground\nrobots with tolerances and acceleration. We: i) Model a robot in differential\ndyn…
View article: A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow Open
Information-flow security is important to the safety and privacy of cyber-physical systems (CPSs) across many domains: information leakage can both violate user privacy and reveal vulnerabilities to physical attacks. CPSs face the challeng…
View article: VeriPhy: verified controller executables from verified cyber-physical system models
VeriPhy: verified controller executables from verified cyber-physical system models Open
We present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that a…
View article: VeriPhy: verified controller executables from verified cyber-physical system models
VeriPhy: verified controller executables from verified cyber-physical system models Open
We present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that a…
View article: CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation
CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation Open
Component-driven proof automation (CDPA) exploits component structure to automate deductive verification of large-scale hybrid systems with non-trivial continuous dynamics. We use CDPA to implement a case study CoasterX, which is a toolcha…
View article: TWAM: A Certifying Abstract Machine for Logic Programs
TWAM: A Certifying Abstract Machine for Logic Programs Open
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 simply-typed dialect of Prolog we call T-Prolog. The crux of…
View article: Formally verified differential dynamic logic
Formally verified differential dynamic logic Open
peer reviewed