Abstract

I will survey the classical, real-time, and time-bounded theories of verification, highlighting key differences and similarities among them, and giving an overview presentation of the solution to a longstanding open problem in the field.

This is joint work with Alex Rabinovich and James Worrell.

Joel Ouaknine is a tenured Reader [roughly equivalent to Associate Professor in North America] in Computer Science at Oxford University, and a Fellow of St John’s College. He holds a B.Sc. and M.Sc. in Mathematics from McGill University, and received his Ph.D. in Computer Science from Oxford in 2001. He subsequently did postdoctoral work at Tulane University and Carnegie Mellon University. In 2009 he was awarded an EPSRC Leadership Fellowship, which relieves him of teaching and administrative duties for a period of five years, and the following year he received the 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 real-time and probabilistic systems, verification (especially software model checking), concurrency, logic, and automata theory.