Skip to main navigation
Skip to Content
Computer Science
University of Toronto
Quercus
Student Support
Contact
About
History of U of T Computer Science
Computer Science at U of T Mississauga
Computer Science at U of T Scarborough
Employment Opportunities for Faculty/Lecturers
How to Find Us
Contact
Undergraduate
Prospective Undergraduates
Current Undergraduates
Graduate
Prospective Graduate Students
Current Graduate Students
Research
Research Areas
Partner with us
People
Faculty
Staff
In Memoriam
Alumni and Friends
Honours & Awards
Women in Computer Science
Graduate Student Society
Undergraduate Student Union
Undergraduate Artificial Intelligence Group
Undergraduate Theory Group
News & Events
News
Events
@DCS Update
Alumni
Donate
You are viewing: >
Home
>
News & Events
>
Events
> Theory Seminar - Aug 14
About
Undergraduate
Graduate
Research
People
News & Events
Theory Seminar - Aug 14
Event date: Wednesday, August 14, 2013, at 11:10 AM
Location: PT 266
Speaker: Kurt Mehlhorn, Max Planck Institute for Informatics and Saarland University
Title: Certifying Computations
Abstract:
I am mostly interested in algorithms for difficult combinatorial and geometric problems: what is the fastest tour from A to B? How to optimally assign jobs to machines? How can a robot move from one location to another one? Algorithms solving such problems are complex and their implementation is error-prone.
How can we make sure that our implementations of such algorithms are reliable? Certifying algorithms are a viable approach towards the goal. A conventional program for computing a function f works as follows. The user feeds an input x to the program and the program returns an output y. A certifying algorithm for f computes y and a witness (proof) w; w proves that the algorithm has not erred for this particular input. The checker C accepts the triple (x,y,w) if and only if w is a valid witness for the equality y =f(x). Certifying algorithms are the design principle for LEDA, the library of efficient data types and algorithms.
In the first part of the talk, we introduce the concept of certifying algorithms. In the second part of the talk, we discuss a certifying algorithm for three-connectivity of graphs. In the third part of the talk, we discuss a framework for the formal verification of certifying computations.