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: | |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/6077 |
| _version_ | 1826216766680858624 |
|---|---|
| author | Arkoudas, Konstantine |
| author_facet | Arkoudas, Konstantine |
| author_sort | Arkoudas, Konstantine |
| collection | MIT |
| description | 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 are used in the certificate,then we can be assured that r is correct. In effect,we obtain a trust reduction: we no longer have to trust the entire computation; we only have to trust the certificate. Typically, the reasoning used in the certificate is much simpler and easier to trust than the entire computation. Certified computation has two main applications: as a software engineering discipline, it can be used to increase the reliability of our code; and as a framework for cooperative computation, it can be used whenever a code consumer executes an algorithm obtained from an untrusted agent and needs to be convinced that the generated results are correct. We propose DPLs (Denotational Proof Languages)as a uniform platform for certified computation. DPLs enforce a sharp separation between logic and control and over versatile mechanicms for constructing certificates. We use Athena as a concrete DPL to illustrate our ideas, and we present two examples of certified computation, giving full working code in both cases. |
| first_indexed | 2024-09-23T16:53:06Z |
| id | mit-1721.1/6077 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:53:06Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/60772019-04-12T08:28:59Z Certified Computation Arkoudas, Konstantine 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 are used in the certificate,then we can be assured that r is correct. In effect,we obtain a trust reduction: we no longer have to trust the entire computation; we only have to trust the certificate. Typically, the reasoning used in the certificate is much simpler and easier to trust than the entire computation. Certified computation has two main applications: as a software engineering discipline, it can be used to increase the reliability of our code; and as a framework for cooperative computation, it can be used whenever a code consumer executes an algorithm obtained from an untrusted agent and needs to be convinced that the generated results are correct. We propose DPLs (Denotational Proof Languages)as a uniform platform for certified computation. DPLs enforce a sharp separation between logic and control and over versatile mechanicms for constructing certificates. We use Athena as a concrete DPL to illustrate our ideas, and we present two examples of certified computation, giving full working code in both cases. 2004-10-04T14:37:40Z 2004-10-04T14:37:40Z 2001-04-30 AIM-2001-007 http://hdl.handle.net/1721.1/6077 en_US AIM-2001-007 1923011 bytes 286231 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Arkoudas, Konstantine Certified Computation |
| title | Certified Computation |
| title_full | Certified Computation |
| title_fullStr | Certified Computation |
| title_full_unstemmed | Certified Computation |
| title_short | Certified Computation |
| title_sort | certified computation |
| url | http://hdl.handle.net/1721.1/6077 |
| work_keys_str_mv | AT arkoudaskonstantine certifiedcomputation |