@inproceedings{1179fe75c46b466d804edbbf7893825a,
title = "Foundational proof-carrying code",
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.",
keywords = "Application software, Assembly, Java, Kernel, Logic, Mechanical factors, Permission, Program processors, Software safety, Virtual machining",
author = "Appel, {Andrew W.}",
note = "Publisher Copyright: {\textcopyright} 2001 IEEE.; Foundations of Intrusion Tolerant Systems, OASIS 2003 ; Conference date: 01-12-2003",
year = "2003",
doi = "10.1109/FITS.2003.1264926",
language = "English (US)",
series = "Foundations of Intrusion Tolerant Systems, OASIS 2003",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "25--34",
editor = "Lala, {Jaynarayan H.}",
booktitle = "Foundations of Intrusion Tolerant Systems, OASIS 2003",
address = "United States",
}