Abstract

We are witnessing an inter-disciplinary convergence between scientific areas underpinned by model-based reasoning and by data-driven learning. Access to information-rich data has to be traded off with a demand for safety criticality: cyber-physical systems are exemplar applications. In this talk, I shall report on ongoing research in this cross-disciplinary domain at OXCAV, the Oxford Control and Verification group. In particular, I shall present recent work on CEGIS, a “counterexample-guided inductive synthesis” framework for sound synthesis tasks that are relevant for dynamical models, control problems, and software programs. I shall elucidate the ins&outs of the CEGIS framework, and display its workings on a couple of broad problems: synthesis of certificates for dynamical and control models, and hybridisation of nonlinear dynamics for safety verification.

Short bio

Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford, where he also served as Deputy Head. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received a Laurea/Phd degrees from the University of Padua and UC Berkeley. His research work spans logic, probability, control, and AI.

More info

http://www.cs.ox.ac.uk/people/alessandro.abate/