Certified Computation
This paper introduces the notion of certified computation. A certified computation does not only produce a result r, but also a correctness certificate, which is a formal proof that r is correct. This can greatly enhance the credibility of the result: if we trust the axioms and inference rules that...
Main Author: | Arkoudas, Konstantine |
---|---|
Language: | en_US |
Published: |
2004
|
Online Access: | http://hdl.handle.net/1721.1/6077 |
Similar Items
-
Type-alpha DPLs
by: Arkoudas, Konstantine
Published: (2004) -
Simplifying transformations for type-alpha certificates
by: Arkoudas, Konstantine
Published: (2004) -
Type-omega DPLs
by: Arkoudas, Konstantine
Published: (2004) -
Combining diagrammatic and symbolic reasoning
by: Arkoudas, Konstantine
Published: (2005) -
Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses
by: Salcianu, Alexandru, et al.
Published: (2005)