Professor Joël Ouaknine, University of Oxford
Abstract: Our society is becoming increasingly reliant on computer systems; think of mobile phones, SatNav, the Internet, and so on. A modern car typically harbours tens to hundreds of microprocessors, themselves running several tens of million lines of code, controlling such critical components as fuel injection, airbags, and anti-lock braking systems. Many of these devices operate in the background, reacting in real-time to a complex environment, and subject to a wide array of functional and timing constraints. A major modern scientific challenge is to devise effective methodologies for accurately modelling and analysing such real-time computer systems, in order to verify and guarantee that they function as they are intended to.
In this talk, I would like to describe some of the fundamental paradigms and algorithms for reasoning about real-time systems. Perhaps surprisingly, several basic questions of decidability and complexity turn out to be remarkably difficult, and a number of problems remain open after some two decades of work in the field. I will present, at a high level, some of the deep connections that are found between real-time verification and mathematical logic, automata theory, combinatorics, and graph theory.
Finally, I will discuss how we expect to translate parts of the rich body of theoretical work in real-time systems into concrete engineering achievements, in the context of ongoing collaborations with industrial partners from the automotive and avionics sectors.
Bio: Joel Ouaknine is Professor of Computer Science at Oxford University, and a Fellow of St John’s College. He holds a BSc and MSc in Mathematics from McGill University, and received his PhD in Computer Science from Oxford in 2001. He subsequently did postdoctoral work at Tulane University and Carnegie Mellon University, and more recently held visiting positions at the Ecole Normale Superieure in Cachan, France. In both 2007 and 2008 he received an Outstanding Teaching Award from Oxford University, and the following year he was awarded an EPSRC Leadership Fellowship, enabling him to focus (almost) exclusively on research for a period of five years. He is the recipient of the 2010 Roger Needham Award, given annually "for a distinguished research contribution in Computer Science by a UK-based researcher within ten years of his or her PhD." His research interests include the verification of real-time, probabilistic, and infinite-state systems (e.g. model-checking algorithms, decision problems, complexity), logic and applications to verification, software analysis, concurrency, and automata theory.
Event Information
The meeting is on Thursday 17 May, 7.00 for 7.30 and ends around 9.00.
It will be held at the Oxford e-Research Centre, 6 Keble Road, Oxford OX1 3QG.
Sandwiches and light refreshments are available from 7.00pm.
Meetings are open to non-members and free.
