### 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) |
---|---|

Title of host publication | Proceedings - Symposium on Logic in Computer Science |

Pages | 247-256 |

Number of pages | 10 |

State | Published - Jan 1 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 | United States |

City | Boston, MA |

Period | 6/16/01 → 6/19/01 |

### All Science Journal Classification (ASJC) codes

- Software
- Mathematics(all)

## Fingerprint Dive into the research topics of 'Foundational proof-carrying code'. Together they form a unique fingerprint.

## Cite this

Appel, A. W. (2001). Foundational proof-carrying code. In

*Proceedings - Symposium on Logic in Computer Science*(pp. 247-256)