3 papers
cs.LO2026
Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
Enguerrand Prebet, André Platzer
Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to…
eess.SY2025
Verification of Autonomous Neural Car Control with KeYmaera X
Enguerrand Prebet, Samuel Teuber, André Platzer
This article presents a formal model and formal safety proofs for the ABZ'25 case study in differential dynamic logic (dL). The case study considers an autonomous car driving on a…
cs.LO2024
Uniform Substitution for Differential Refinement Logic
Enguerrand Prebet, André Platzer
This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneousl…