Termination of Linear Loops: Advances and Challenges
Event details
| Date | 01.07.2015 |
| Hour | 14:15 › 15:30 |
| Speaker |
Prof. Joel Ouaknine, Oxford University Bio: Joel Ouaknine is Professor of Computer Science at Oxford University, and 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 a visiting professorship 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." In 2015, he was awarded an ERC Consolidator Grant, again allowing him to focus mainly on research for a five-year period. His research interests include the automated verification of real-time, probabilistic, and infinite-state systems (e.g. model-checking algorithms, synthesis problems, complexity), logic and applications to verification, decision and synthesis problems for linear dynamical systems, automated software analysis, concurrency, and theoretical computer science. |
| Location | |
| Category | Conferences - Seminars |
In the quest for automated program analysis and verification, program termination -- determining whether a given program will always halt or could execute forever -- has emerged as a central component. Although proven undecidable in the general case by Alan Turing over 80 years ago, positive results have been obtained in a number of restricted instances, from simple counter machines to Windows device drivers. In this talk, I survey the situation with a focus on simple linear programs, i.e., WHILE loops in which all assignments and guards are linear. Somewhat surprisingly, the study of termination of simple linear programs involves advanced techniques from a variety of mathematical fields, including analytic and algebraic number theory, Diophantine geometry, and real algebraic geometry. I will present an overview of known results, and discuss existing algorithmic challenges and open problems.
Speaker’s home page:
http://www.cs.ox.ac.uk/joel.ouaknine/home.html
Speaker’s home page:
http://www.cs.ox.ac.uk/joel.ouaknine/home.html
Practical information
- General public
- Free