VMCAI 2025
Mon 20 - Tue 21 January 2025 Denver, Colorado, United States
co-located with POPL 2025

Feed-forward controllers compute control outputs to adapt to changing environment parameters in a cyber-physical system. When synthesizing control functions it can be difficult to give an analytical description of the controlled plant or to decide the expected control output ahead of time. These systems must, however, adhere to strict safety requirements, which makes it hard to write correct controllers. In this paper, we propose a novel blackbox synthesis approach to construct a continuous control function while dynamically sampling a limited number of test cases. The controller is guaranteed to be correct for a given Lipschitz bound. It can be adapted to work for increasingly conservative estimates of the bound based on observed behavior, iteratively providing increasing confidence in its correctness. Our algorithm employs a linear interpolation model, based on a Delaunay triangulation, to identify candidate control functions. It then generates additional test cases to either confirm a candidate or to improve the model. We evaluate our approach on random benchmarks and CPS examples to show its effectiveness.

Mon 20 Jan

Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30
Keynote Talk and Cyber-Physical SystemsVMCAI 2025 at Hopscotch
Chair(s): Sriram Sankaranarayanan University of Colorado, Boulder
09:00
60m
Talk
Keynote Talk: Formal methods in a model-free, data-driven world
VMCAI 2025
Jyotirmoy Deshmukh University of Southern California
10:00
30m
Talk
Synthesis of Controllers for Continuous Blackbox Systems
VMCAI 2025
Benedikt Maderbacher Graz University of Technology, Felix Windisch Graz University of Technology, Alberto Larrauri University of Oxford, Roderick Bloem Institute of Software Technology, Graz University of Technology