English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  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

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0010-12BF-E Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0019-85B5-1
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Alkassar, Eyad1, Author
Böhme, Sascha2, Author
Mehlhorn, Kurt3, Author           
Rizkallah, Christine3, Author           
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              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2011-11-162011
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 618673
DOI: 10.1007/978-3-642-22110-1_7
URI: http://www.mpi-inf.mpg.de/~mehlhorn/ftp/VerificationCertComps.pdf
Other: Local-ID: C1256428004B93B8-5C01AA7BBEAB7C26C125785C003095BF-FormalVerificationofCertifyingComputations
 Degree: -

Event

show
hide
Title: CAV 2011
Place of Event: Snowbird, Utah, USA
Start-/End Date: 2011-07-14 - 2011-07-20

Legal Case

show

Project information

show

Source 1

show
hide
Title: Computer Aided Verification
  Subtitle : 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings
Source Genre: Proceedings
 Creator(s):
Gopalakrishnan, Ganesh1, Editor
Qadeer, Shaz1, Editor
Affiliations:
1 External Organizations, ou_persistent22            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 67 - 82 Identifier: ISBN: 978-3-642-22109-5

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 6806 Sequence Number: - Start / End Page: - Identifier: -