DocumentCode
3223416
Title
Foundational proof-carrying code
Author
Appel, Andrew W.
Author_Institution
Princeton Univ., NJ, USA
fYear
2001
fDate
2001
Firstpage
247
Lastpage
256
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on
Conference_Location
Boston, MA
ISSN
1043-6871
Print_ISBN
0-7695-1281-X
Type
conf
DOI
10.1109/LICS.2001.932501
Filename
932501
Link To Document