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
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 22 October 2013
13:30
30 Minutes
E1 4
024
Saarbrücken
Abstract
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.
Contact
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.
Christine Rizkallah, 10/17/2013 13:24 -- Created document.