Foundational proof-carrying code
Top Cited Papers
- 13 November 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 41, 247-256
- https://doi.org/10.1109/lics.2001.932501
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 ip-sos 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
This publication has 15 references indexed in Scilit:
- Principled scavengingPublished by Association for Computing Machinery (ACM) ,2001
- Typed memory management via static capabilitiesACM Transactions on Programming Languages and Systems, 2000
- A certifying compiler for JavaPublished by Association for Computing Machinery (ACM) ,2000
- Machine Instruction Syntax and Semantics in Higher Order LogicPublished by Springer Nature ,2000
- Flexible type analysisPublished by Association for Computing Machinery (ACM) ,1999
- From system F to typed assembly languageACM Transactions on Programming Languages and Systems, 1999
- System Description: Twelf — A Meta-Logical Framework for Deductive SystemsPublished by Springer Nature ,1999
- Specifying representations of machine instructionsACM Transactions on Programming Languages and Systems, 1997
- Elf: A meta-language for deductive systemsPublished by Springer Nature ,1994
- A framework for defining logicsJournal of the ACM, 1993