Polyvios Pratikakis, Verifying Array Bounds Check Elimination in Bartok
Singularity is a research operating system that makes heavy use of language properties such as memory safety, type soundness, etc. So far, each such property is checked during compilation. However, the long term goal for singularity is to adopt a proof-carrying code design, where the compiler generates proofs for each property it checks. Then, a simple verifier checks the proofs before running the program, thus greatly reducing the size of the trusted code. To this end, we developed a proof verifier for CLIC, an expressive proof language based on the Calculus of Inductive Constructions with linear types. In addition, and as a proof-of-concept example, we developed a a verification condition generator for a simple safety property, namely that all array accesses are within bounds. Using this framework we were able to verify programs with hand-written proofs. Finally, we started working on automatically generating such proofs in the Bartok compiler.
A useful primer on the Curry-Howard isomorphism, which underlies the proof technique in this work, see Wadler.