Abstract
Proof-carrying code is a framework for the mechanical verification of safety properties of machine language programs, but the problem arises of quis custodiat ipsos custodes-who will verify the verifier itself? Foundational proof-carrying code is verification from the smallest possible set of axioms, using the simplest possible verifier and the smallest possible runtime system. I will describe many of the mathematical and engineering problems to be solved in the construction of a foundational proof-carrying code system.
| Original language | English (US) |
|---|---|
| Pages | 247-256 |
| Number of pages | 10 |
| State | Published - 2001 |
| Event | 16th Annual IEEE Symposium on Logic in Computer Science - Boston, MA, United States Duration: Jun 16 2001 → Jun 19 2001 |
Other
| Other | 16th Annual IEEE Symposium on Logic in Computer Science |
|---|---|
| Country/Territory | United States |
| City | Boston, MA |
| Period | 6/16/01 → 6/19/01 |
All Science Journal Classification (ASJC) codes
- Software
- General Mathematics