1

Learning One-Clock Timed Automata
We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework …
PDF Cite Slides DOI Artifact Evaluated Best Paper Award @ FMAC 2019 Springer High-Impact Paper
Learning One-Clock Timed Automata
NIL: Learning Nonlinear Interpolants
Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model …
PDF Cite Code Slides DOI
NIL: Learning Nonlinear Interpolants
Taming Delays in Dynamical Systems
Delayed coupling between state variables occurs regularly in technical dynamical systems, especially embedded control. As it …
PDF Cite Slides DOI Artifact Evaluated
Taming Delays in Dynamical Systems
What's to Come is Still Unsure
The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and …
PDF Cite Code Slides Video DOI Distinguished Paper Award
What's to Come is Still Unsure
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations
Delays in feedback control loop, as induced by networked distributed control schemes, may have detrimental effects on control …
PDF Cite Slides Video DOI
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations
A Two-Way Path between Formal and Informal Design of Embedded Systems
It is well known that informal simulation-based design of embedded systems has a low initial cost and delivers early results; yet it …
PDF Cite Code Slides DOI
A Two-Way Path between Formal and Informal Design of Embedded Systems
Validated Simulation-Based Verification of Delayed Differential Dynamics
Verification by simulation, based on covering the set of time-bounded trajectories of a dynamical system evolving from the initial …
PDF Cite Code Poster Slides DOI
Validated Simulation-Based Verification of Delayed Differential Dynamics
Computing Reachable Sets of Linear Vector Fields Revisited
The reachability problem is one of the most important issues in the verification of hybrid systems. But unfortunately the reachable …
PDF Cite Code Slides DOI
Computing Reachable Sets of Linear Vector Fields Revisited
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and …
PDF Cite Code Slides DOI
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
Decidability of the Reachability for a Family of Linear Vector Fields
The reachability problem is one of the most important issues in the verification of hybrid systems. Computing the reachable sets of …
PDF Cite Code Slides DOI
Decidability of the Reachability for a Family of Linear Vector Fields