Blogs

Machine Learning Blog

Monthly Archives: October 2017

ML seminar, Fri 20 Oct, 1pm

News, Seminar.

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

Find us

City, University of London

Northampton Square

London EC1V 0HB

United Kingdom

Back to top

City, University of London is an independent member institution of the University of London. Established by Royal Charter in 1836, the University of London consists of 18 independent member institutions with outstanding global reputations and several prestigious central academic bodies and activities.