MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Alkassar, Eyad
Böhme, Sascha
Mehlhorn, Kurt
Rizkallah, Christine		dblp
dblp
dblp
dblp
Not MPG Author(s):
Alkassar, Eyad
Böhme, Sascha
Editor(s):
Gopalakrishnan, Ganesh
Qadeer, Shaz		dblp
dblp
Not MPII Editor(s):
Gopalakrishnan, Ganesh
Qadeer, Shaz
BibTeX cite key*:
FormalVerificationofCertifyingComputations
Title, Booktitle
Title*:
Verification of Certifying Computations
Booktitle*:
Computer Aided Verification : 23rd International Conference, CAV 2011
Event, URLs
Conference URL::
http://www.cs.utah.edu/events/conferences/cav2011/
Downloading URL:
http://www.mpi-inf.mpg.de/~mehlhorn/ftp/VerificationCertComps.pdf
Event Address*:
Snowbird, USA
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
14 July 2011
Event End Date:
20 July 2011
Publisher
Name*:
Springer
URL:
http://www.springer.com/
Address*:
Heidelberg
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
6806
Number:
Month:
Pages:
67-82
Year*:
2011
VG Wort Pages:
ISBN/ISSN:
978-3-642-22109-5
Sequence Number:
DOI:
10.1007/978-3-642-22110-1_7
Note, Abstract, ©
(LaTeX) Abstract:
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 paper we develop a framework to seamlessly 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 demonstrate the
effectiveness of our approach by applying it to the verification of
the algorithmic library LEDA.
Keywords:
Certifying Verification LEDA Isabelle VCC
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Algorithms and Complexity Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{FormalVerificationofCertifyingComputations,
AUTHOR = {Alkassar, Eyad and B{\"o}hme, Sascha and Mehlhorn, Kurt and Rizkallah, Christine},
 EDITOR = {Gopalakrishnan, Ganesh and Qadeer, Shaz},
 TITLE = {Verification of Certifying Computations},
 BOOKTITLE = {Computer Aided Verification : 23rd International Conference, CAV 2011},
 PUBLISHER = {Springer},
 YEAR = {2011},
 VOLUME = {6806},
 PAGES = {67--82},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Snowbird, USA},
 ISBN = {978-3-642-22109-5},
 ISBN = {0302-9743},
 DOI = {10.1007/978-3-642-22110-1_7},
}

Entry last modified by Anja Becker, 11/16/2011
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]		Created
03/23/2011 09:50:40
Revisions
3.
2.
1.
0.
Editor(s)
Anja Becker
Thomas Sauerwald
Thomas Sauerwald
Christine Rizkallah
Edit Dates
16.11.2011 15:08:42
03/23/2011 04:32:36 PM
03/23/2011 04:26:27 PM
03/23/2011 09:50:40 AM