The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

An Open Framework for Foundational Proof-Carrying Code

Last modified: Mon Jan 29 18:14:15 2007 GMT.

Authors

Xinyu Feng
Zhaozhong Ni
Zhong Shao
Yu Guo

Abstract

Today's software systems often use many different computation features and span different abstraction levels (e.g., user code and runtime-system code). To build foundational certified systems, it is hard to have a single verification system supporting all computation features. In this paper we present an open framework for foundational proof-carrying code (FPCC). It allows program modules to be specified and certified separately using different type systems or program logics. Certified modules (i.e., code and proof) can be linked together to build fully certified systems. The framework supports modular verification and proof reuse. It is also expressive enough so that invariants established in specific verification systems are preserved even when they are embedded into our framework. Our work presents the first FPCC framework that systematically supports interoperation between different verification systems. It is fully mechanized in the Coq proof assistant with machine-checkable soundness proof.

Published

  • In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07), Nice, France, pages 67-78, January 2007. ©2007 ACM.


  • Technical Report YALEU/DCS/TR-1373 (Extended Version)


  • Coq Implementations [73k]

  • Copyright © 1996-2024 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon