Campus Event Calendar

Event Entry

What and Who

Progress on Verification of Certifying Computations

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

Date, Time and Location

Tuesday, 22 October 2013
30 Minutes
E1 4


Verifying the implementation of complex algorithms in reasonable time goes beyond the state of the art of current verification tools. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for a certifying algorithm checks the witness for correctness and is usually much simpler than the algorithm. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted.

We verified several checkers from the algorithmic library LEDA using the interactive theorem prover Isabelle/HOL as a backend to the automatic code verifier VCC. Currently, using newly developed tools, we show that the verification can be carried out completely within Isabelle/HOL.

In this talk I will give an overview of both approaches and a comparison.


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

Christine Rizkallah, 10/17/2013 13:29
Christine Rizkallah, 10/17/2013 13:24 -- Created document.