Published papers, technical reports, and talks online.


Xinyu Feng
Zhaozhong Ni
Zhong Shao
Yu Guo


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.


  • 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]