A Framework for the Verification of Certifying Computations

Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually involves intricate mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2014-03, Vol.52 (3), p.241-273
Main Authors: Alkassar, Eyad, Böhme, Sascha, Mehlhorn, Kurt, Rizkallah, Christine
Format: Article
Language:English
Subjects:
Algorithms
Applied sciences
Artificial Intelligence
Checkers
Computation
Computer Science
Computer science
control theory
systems
Computer systems performance. Reliability
Exact sciences and technology
Interactive
Leda
Logic and foundations
Logical, boolean and switching functions
Mathematical analysis
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Mathematical logic, foundations, set theory
Mathematical models
Mathematics
Program verification (computers)
Proof theory and constructive mathematics
Sciences and techniques of general use
Software
Symbolic and Algebraic Manipulation
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually involves intricate 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. The verification of checkers is feasible with current tools and leads to computations that can be completely trusted. We describe a framework to seamlessly verify certifying computations. We use the automatic verifier VCC for establishing the correctness of the checker and the interactive theorem prover Isabelle/HOL for high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of typical examples of the industrial-level and widespread algorithmic library LEDA.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-013-9289-2