Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




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

URL of the conference:

http://www.cs.utah.edu/events/conferences/cav2011/

URL for downloading the paper:

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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 AM
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section