"Proving Programs Terminate using Well Orderings, Ramsey Theory, and Matrices""Proving Programs Terminate using Well Orderings, Ramsey Theory, and Matrices"http://www.haverford.edu/calendar/details/229191KINSC Hilles Computer Lab2013-02-11T16:15:002013-02-11T18:00:00
February 11, 4:15PM
KINSC Hilles Computer Lab
Talk by Bill Gasarch, Professor of Computer Science, University of Maryland College Park
Description
You have just written a program! The user may input data several times during its execution. But the user is a wise-ass---- he wants to input data to make the program run FOREVER! You want to make sure that he can't do that. You want to PROVE that NO MATTER what the wise-ass-user inputs, the program WILL terminate. We show several ways to prove that, NO MATTER WHAT WISE-ASS does, the program will terminate. Serves him right! We use mathematics of interest: well orderings, Ramsey Theory, and Matrices. These techniques are used by many REAL program checkers. No knowledge of well ordersing, Ramsey Theory, or Matrices will be assumed. ------------------------------------- Dr. William Gasarch got his BS in Math and Applied Math (so he is well rounded!) from SUNY Stonybrook in 1989 and his PhD in Computer science from Harvard in 1985. He has been at the University of Maryland at College Park CS dept from 1986 until... NOW. His main interests are logic and Ramsey Theory. He got interested in the topic of todays talk because there was a CACM article about it that he read and tracked references and followed up on. Lesson: Follow up on what interests you!
Tea at 4:00PM
For More Info
John P Dougherty
610-896-4993
addr
Responsible at Event
JD