Campus Event Calendar

Event Entry

New for: D3

What and Who

Verification of Certifying Computations

Christine Rizkallah
Max-Planck-Institut für Informatik - D1
AG1 Mittagsseminar (own work)
AG 1, AG 3, AG 5, SWS, AG 4, RG1, MMCI  
AG Audience

Date, Time and Location

Friday, 26 August 2011
30 Minutes
E1 4


Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current verification tools and proving their correctness usually involves non-trivial mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm – yet it is all the user has to trust. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted. In this talk I will present a framework that we developed to verify certifying computations. The automatic verifier VCC is used for checking code correctness, and the interactive theorem prover Isabelle/HOL targets high-level mathematical properties of algorithms. We demonstrated our approach by presenting the verification of a typical example of the algorithmic library LEDA.

Joint work with Eyad Alkassar, Sascha Böhme, and Kurt Mehlhorn. This work was published at CAV this year.


Christine Rizkallah
--email hidden
passcode not visible
logged in users only

Christine Rizkallah, 08/16/2011 10:42
Christine Rizkallah, 08/12/2011 14:51
Christine Rizkallah, 08/12/2011 14:50 -- Created document.