activity
20172025
most citedThe KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving

29 citations · 70 across the 8 of their papers we have counts for

collaborators
Showing 2023Show all

5 papers · 1 filter

eess.SY2023

CESAR: Control Envelope Synthesis via Angelic Refinements

Aditi Kabra, Jonathan Laurent, Stefan Mitsch +1

This paper presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to…

cs.FL2023

A Usage-Aware Sequent Calculus for Differential Dynamic Logic

Myra Dotzel, Stefan Mitsch, André Platzer

Ensuring that safety-critical applications behave as intended is an important yet challenging task. Modeling languages like differential dynamic logic (dL) have proof calculi capab…

cs.LO2023

Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars

Megan Strauss, Stefan Mitsch

Technology advances give us the hope of driving without human error, reducing vehicle emissions and simplifying an everyday task with the future of self-driving cars. Making sure t…

cs.LO20233 cited

Dynamic Logic of Communicating Hybrid Programs

Marvin Brieger, Stefan Mitsch, André Platzer

This paper presents a dynamic logic for compositional deductive verification of communicating hybrid programs (CHPs). CHPs go beyond the traditional mixed…

cs.LO2023

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

Marvin Brieger, Stefan Mitsch, André Platzer

This paper introduces a uniform substitution calculus for , the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious pr…