Name
Abstract | ||
|---|---|---|
Result checking is a general methodology for ensuring that untrusted computations are valid. Its essence lies in defining efficient checking procedures to verify that a result satisfies some expected property. Result checking often relies on certificates to make the verification process efficient, and thus involves two strongly connected tasks: the generation of certificates and the implementation of a checking procedure. Several ad-hoc solutions exist, but they differ significantly on the kind of properties involved and thus on the validation procedure. The lack of common methodologies has been an obstacle to the applicability of result checking to a more comprehensive set of algorithms. We propose the first framework for building result checking infrastructures for a large class of properties, and illustrate its generality through several examples. The framework has been implemented in Haskell. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-12251-4_7 | FLOPS |
Keywords | Field | DocType |
result checking infrastructure,comprehensive set,result checking,functional framework,general methodology,expected property,validation procedure,checking procedure,efficient checking procedure,ad-hoc solution,common methodology,satisfiability | Abstraction model checking,Model checking,Functional programming,Computer science,Algorithm,Automated proof checking,Theoretical computer science,Haskell,Strongly connected component,Sorting algorithm,Proof assistant | Conference |
Volume | ISSN | ISBN |
6009 | 0302-9743 | 3-642-12250-7 |
Citations | PageRank | References |
1 | 0.35 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| Pablo Buiras | 2 | 112 | 6.13 |
| César Kunz | 3 | 167 | 10.81 |