29 citations · 67 across the 4 of their papers we have counts for
4 papers · 1 filter
Implicit and Explicit Proof Management in KeYmaera X
Stefan Mitsch
Hybrid systems theorem proving provides strong correctness guarantees about the interacting discrete and continuous dynamics of cyber-physical systems. The trustworthiness of proof…
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Simon Lunel, Stefan Mitsch, Benoit Boyer +1
Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart…
Verified Runtime Validation for Partially Observable Hybrid Systems
Stefan Mitsch, André Platzer
Formal verification provides strong safety guarantees but only for models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physica…
The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving
Stefan Mitsch, André Platzer
Hybrid systems verification is quite important for developing correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered…