Foundational proof-carrying code

Research output: Chapter in Book/Report/Conference proceedingConference contribution

177 Scopus citations


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 languageEnglish (US)
Title of host publicationProceedings - Symposium on Logic in Computer Science
Number of pages10
StatePublished - Jan 1 2001
Event16th Annual IEEE Symposium on Logic in Computer Science - Boston, MA, United States
Duration: Jun 16 2001Jun 19 2001


Other16th Annual IEEE Symposium on Logic in Computer Science
CountryUnited States
CityBoston, MA

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)