Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  Verification of Certifying Computations

Alkassar, E., Böhme, S., Mehlhorn, K., & Rizkallah, C. (2011). Verification of Certifying Computations. In G. Gopalakrishnan, & S. Qadeer (Eds.), Computer Aided Verification (pp. 67-82). Berlin: Springer.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Alkassar, Eyad1, Autor
Böhme, Sascha2, Autor
Mehlhorn, Kurt3, Autor           
Rizkallah, Christine3, Autor           
Affiliations:
1Cluster of Excellence Multimodal Computing and Interaction, ou_persistent22              
2External Organizations, ou_persistent22              
3Algorithms and Complexity, MPI for Informatics, Max Planck Society, ou_24019              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2011-11-162011
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 618673
DOI: 10.1007/978-3-642-22110-1_7
URI: http://www.mpi-inf.mpg.de/~mehlhorn/ftp/VerificationCertComps.pdf
Anderer: Local-ID: C1256428004B93B8-5C01AA7BBEAB7C26C125785C003095BF-FormalVerificationofCertifyingComputations
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: CAV 2011
Veranstaltungsort: Snowbird, Utah, USA
Start-/Enddatum: 2011-07-14 - 2011-07-20

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Computer Aided Verification
  Untertitel : 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings
Genre der Quelle: Konferenzband
 Urheber:
Gopalakrishnan, Ganesh1, Herausgeber
Qadeer, Shaz1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 67 - 82 Identifikator: ISBN: 978-3-642-22109-5

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
  Kurztitel : LNCS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 6806 Artikelnummer: - Start- / Endseite: - Identifikator: -