1

Does a Program Yield the Right Distribution?
We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the …
PDF Cite DOI Artifact Evaluated
Does a Program Yield the Right Distribution?
Latticed $k$-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques, $k$-induction and bounded model checking (BMC), in the more general setting of …
PDF Cite Slides DOI Artifact Evaluated Pulp Fiction
Latticed $k$-Induction with an Application to Probabilistic Programs
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence …
PDF Cite Slides Video DOI Artifact Evaluated
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety …
PDF Cite Slides Video DOI Artifact Evaluated Pulp Fiction
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
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