Please use this identifier to cite or link to this item:
http://dspace.mediu.edu.my:8181/xmlui/handle/1721.1/6077Full metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.creator | Arkoudas, Konstantine | - |
| dc.date | 2004-10-04T14:37:40Z | - |
| dc.date | 2004-10-04T14:37:40Z | - |
| dc.date | 2001-04-30 | - |
| dc.date.accessioned | 2013-10-09T02:42:45Z | - |
| dc.date.available | 2013-10-09T02:42:45Z | - |
| dc.date.issued | 2013-10-09 | - |
| dc.identifier | AIM-2001-007 | - |
| dc.identifier | http://hdl.handle.net/1721.1/6077 | - |
| dc.identifier.uri | http://koha.mediu.edu.my:8181/xmlui/handle/1721 | - |
| dc.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. | - |
| dc.format | 1923011 bytes | - |
| dc.format | 286231 bytes | - |
| dc.format | application/postscript | - |
| dc.format | application/pdf | - |
| dc.language | en_US | - |
| dc.relation | AIM-2001-007 | - |
| dc.title | Certified Computation | - |
| Appears in Collections: | MIT Items | |
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.