Title :
Foundational proof-carrying code
Author :
Appel, Andrew W.
Author_Institution :
Princeton Univ., NJ, USA
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” - i.e. who verifies 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 describe many of the mathematical and engineering problems to be solved in the construction of a foundational proof-carrying code system
Keywords :
machine oriented languages; program verification; programming theory; safety; axioms; engineering problems; foundational proof-carrying code; mathematical problems; mechanical program verification; runtime system; safety properties; verifier verification; Application software; Assembly; Java; Logic; Marketing and sales; Program processors; Safety; Virtual machining;
Conference_Titel :
Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on
Conference_Location :
Boston, MA
Print_ISBN :
0-7695-1281-X
DOI :
10.1109/LICS.2001.932501
