English Version

Modular Certification of Low-level Intermediate Representation Programs
DONG Yuan, WANG Shengyuan, ZHANG Liwei, YANG Ping

Abstract: Modular certification of low-level intermediate representation (IR) programs is one of the key steps of proof-transforming compilation. The major challenges are the complexity of abstract control stack and the lack of control flow structure information due to their flat nature. To tackle these challenges, a novel Hoare-logic like framework for modular certification of p-machine style bytecode IR programs is presented in this paper. This logic can fully support abstract control stack and unstructured control flow for modular certification of IR programs involving while loop, procedure call/return, recursive procedure, and even nested procedure. It applies Foundational Proof-Carrying Code (FPCC) concepts to IR level. This system is expressive and fully mechanized. We prove its soundness and demonstrate its power by certifying the implementation of some IR programs in the Coq proof assistant. This work not only provides a solid theoretical foundation of IR programs reasoning about for abstract machine, but also makes an important advance toward building proof-transforming compilation environment in which certified IR codes with their proofs can be compiled to machine checkable proof-carrying low-level assembly codes.

Key words: Program Modular Certification; Intermediate Representation; Nested Procedure; Hoare-like Logic

Links

COMPSAC09 NCBP: PDF Format

---