Deductive runtime certification

Konstantine Arkoudas and Martin Rinard

Paper: ps , pdf

RV 2004 talk: ps , pdf

Abstract:

This paper introduces a notion of certified computation whereby an algorithm not only produces a result r for a given input x, but also proves that r is a correct result for x. This can greatly enhance the credibility of the result: if we trust the axioms and inference rules that are used in the proof, then we can be assured that r is correct. Typically, the reasoning used in a certified computation is much simpler than the computation itself. We present and analyze two examples of certifying algorithms. We have developed denotational proof languages (DPLs) as a uniform platform for certified computation. DPLs integrate computation and deduction seamlessly, offer strong soundness guarantees, and provide versatile mechanisms for constructing proofs and proof-search methods. We have used DPLs to implement numerous well-known algorithms as certifiers, ranging from sorting algorithms to compiler optimizations, the Hindley-Milner W algorithm, Prolog engines, and more.

BibTeX Entry

@Inproceedings{RV2004ArkoudasAndRinard,
 author		={K. Arkoudas and M. Rinard},
 title		={Deductive runtime certification},
 booktitle	={Proceedings of the 2004 Workshop on Runtime
 Verification (RV 2004)},
 address        = {Barcelona, Spain},  
 month          ={April},
 year		={2004}}

Back to the publication list of Konstantine Arkoudas