6 papers
Oracular Programming: A Modular Foundation for Building LLM-Enabled Software
Jonathan Laurent, André Platzer
Large Language Models (LLMs) can solve previously intractable tasks given only natural-language instructions and a few examples, but they remain difficult to steer precisely and la…
LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game
Aditi Kabra, Jonathan Laurent, Ruben Martins +2
Hybrid games model cyber-physical systems (CPS), like cars, trains, and airplanes, where discrete control decisions interact with continuous physical dynamics. We use Large Languag…
Can Large Language Models Autoformalize Kinematics?
Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj +3
Autonomous cyber-physical systems like robots and self-driving cars could greatly benefit from using formal methods to reason reliably about their control decisions. However, befor…
Complete Dynamic Logic of Communicating Hybrid Programs
Marvin Brieger, Stefan Mitsch, André Platzer
This article presents a relatively complete proof calculus for the dynamic logic of communicating hybrid programs dLCHP. Beyond hybrid systems, communicating hybrid programs not on…
Hybrid Game Control Envelope Synthesis
Aditi Kabra, Jonathan Laurent, Stefan Mitsch +1
Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to…
Adaptive Shielding via Parametric Safety Proofs
Yao Feng, Jun Zhu, André Platzer +1
A major challenge to deploying cyber-physical systems with learning-enabled controllers is to ensure their safety, especially in the face of changing environments that necessitate…