Machine Learning

When: Fri, 20 Oct 2017,
Where: AG24a, College Building

Who: Alessandro Abate, University of Oxford

Title: Data-driven and model-based quantitative verification of physical systems

Abstract: In this seminar I discuss a new and formal, measurement-driven and model-based automated verification technique, to be applied on quantitative properties over systems with partly unknown dynamics. I focus on physical systems (with spatially continuous variables, possibly noisy), driven by external inputs and accessed under noisy measurements. I formulate this new setup as a data-driven Bayesian model inference problem, formally embedded within a quantitative, model-based verification procedure.

Who: Lucas Cordeiro, University of Oxford

Title: DSSynth: An Automated Digital Controller Synthesis Tool for Physical Plants

Abstract: We present an automated MATLAB Toolbox, named DSSynth (Digital-System Synthesizer), to synthesize sound digital controllers for physical plants that are represented as linear time invariant systems with single input and output. In particular, DSSynth synthesizes digital controllers that are sound w.r.t. stability and safety specifications. DSSynth considers the complete range of approximations, including time discretization, quantization effects and finite-precision arithmetic (and its rounding errors). We demonstrate the practical value of this toolbox by automatically synthesizing and safe controllers for intricate physical plant models from the digital control literature. The resulting toolbox enables the application of program synthesis to real- control engineering problems. A demonstration can be found at hLQslRcee8.

Who: Cristina David, University of Oxford

Title: Solving Second-Order Constraints with Program Synthesis

Abstract: In this talk I’ll summarise our work on expressing and solving program analysis problems as second-order satisfiability. I’ll start by introducing a fragment of second-order logic that is expressive enough to capture numerous program analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, refactoring). Subsequently, I will describe the solver we built for this fragment, which is based on program synthesis. In particular, our synthesiser is an instance of the Counterexample Guided Inductive Synthesis (CEGIS) framework and makes use of symbolic bounded model checking and genetic programming. I’ll end by discussing in more detail one of the areas where we’ve successfully applied our synthesiser, namely the synthesis of safe digital feedback controllers for physical plants represented as linear, time-invariant models.

All are welcome!

Artur Garcez

Source link


Please enter your comment!
Please enter your name here