Paper Info
Title
An Introduction To Certifying Algorithms
Abstract
A certifying algorithm is an algorithm that produces, with each output, a certificate or witness that the particular output is correct. A user of a certifying algorithm inputs x, receives the output y and the certificate w, and then checks, either manually or by use of a program, that w proves that y is a correct output for input x. In this way, he/she can be sure of the correctness of the output without having to trust the algorithm. We put forward the thesis that certifying algorithms are much superior to non- certifying algorithms, and that for complex algorithmic tasks, only certifying algorithms are satisfactory. Acceptance of this thesis would lead to a change of how algorithms are taught and how algorithms are researched. The widespread use of certifying algorithms would greatly enhance the reliability of algorithmic software. We also demonstrate that the formal verification of result checkers is within the reach of current verification technology. The combination of certifying algorithms and formal verification of result checkers leads to formally verified computations.
Year
DOI
Venue
2011
10.1524/itit.2011.0655
IT-INFORMATION TECHNOLOGY
Keywords
Field
DocType
D.2.5 [Software: Software Engineering: Software/Program Verification], D.2.5 [Software: Software Engineering: Testing and Debugging], certifying algorithms
Software engineering,Computer science,Embedded system
Journal
Volume
Issue
ISSN
53
6
1611-2776
Citations 
PageRank 
References 
0
0.34
6
Authors
5
Name
Order
Citations
PageRank
Eyad Alkassar126622.49
Sascha Böhme221612.94
Kurt Mehlhorn35314853.36
Christine Rizkallah47514.05
Pascal Schweitzer521416.94