Algorithm-independent framework for verifying integer constraints

Last modified: Wed Jun 7 18:46:08 2000 GMT.

Authors

Abstract

Proof-carrying code (PCC), as pioneered by Necula and Lee, allows a code producer to provide a compiled program to a host, along with a formal proof of safety. The PCC-based systems often rely on solving integer constraints to prove the soundness of the index types and to control resource consumption. Unfortunately, existing approaches often require the inclusion of an oracle-like constraints solver in the trusted computing base (TCB) or at least lock the safety policy with one particular solver. This paper presents a feasibility study for disassociating the constraints solver from the TCB and the safety policy from the actual solver algorithm. To demonstrate this, we produce a simple framework, show how to adapt the popular solvers such as the Omega test and the Simplex method into this framework, and study some of its properties.

Submitted for publication.
- Gzipped Postscript [123k]
- PDF [178k]
- BibTeX Entry
Technical Report
- Gzipped Postscript [210k]
- PDF [309k]
- BibTeX Entry

colophon