BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Termination of Linear Loops: Advances and Challenges
DTSTART:20150701T141500
DTEND:20150701T153000
DTSTAMP:20260916T050003Z
UID:786f689ba02e2dda96071fbb15a6db625d523e156831518e2f164245
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. Joel Ouaknine\, Oxford University\nBio: Joel Ouaknine is
  Professor of Computer Science at Oxford University\, and Fellow of St Joh
 n'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 subsequ
 ently did postdoctoral work at Tulane University and Carnegie Mellon Unive
 rsity\, and more recently held a visiting professorship at the Ecole Norma
 le Superieure in Cachan\, France. In both 2007 and 2008 he received an Out
 standing Teaching Award from Oxford University\, and the following year he
  was awarded an EPSRC Leadership Fellowship\, enabling him to focus (almos
 t) exclusively on research for a period of five years. He is the recipient
  of the 2010 Roger Needham Award\, given annually "for a distinguished res
 earch 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 Gr
 ant\, again allowing him to focus mainly on research for a five-year perio
 d. His research interests include the automated verification of real-time\
 , probabilistic\, and infinite-state systems (e.g. model-checking algorith
 ms\, synthesis problems\, complexity)\, logic and applications to verifica
 tion\, decision and synthesis problems for linear dynamical systems\, auto
 mated software analysis\, concurrency\, and theoretical computer science.\
 nIn the quest for automated program analysis and verification\, program te
 rmination -- determining whether a given program will always halt or could
  execute forever -- has emerged as a central component. Although proven un
 decidable in the general case by Alan Turing over 80 years ago\, positive 
 results have been obtained in a number of restricted instances\, from simp
 le 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 s
 tudy 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 c
 hallenges and open problems.\nSpeaker’s home page:  http://www.cs.ox.ac
 .uk/joel.ouaknine/home.html
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR