Machine Learning seminar
When: Fri, 20 Oct 2017, 1pm
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 stable and safe controllers for intricate physical plant models from the digital control literature. The resulting toolbox enables the application of program synthesis to real-world control engineering problems. A demonstration can be found at https://youtu.be/ 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
