Modular Certification of Low-Level Intermediate Representation Programs

Modular certification of low-level intermediate representation (IR) programs is one of the key steps of proof-transforming compilation. The major challenges are lexity of abstract control stacks and the lack of control flow information due to their flat nature. To tackle these challenges, we present in this paper a novel Hoare-style logic framework for modular certification of p-machine style as IR programs. This logic can fully support abstract control stacks and unstructured control flows for modular certification of IR programs involving while loops, procedure call/return, recursive procedures, and even nested procedures. 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 for reasoning about IR programs, but also makes an import...

• Type: Conference
• Year: 2009
• Where: COMPSAC
• Authors: Yuan Dong, Shengyuan Wang, Liwei Zhang, Ping Yang
• Keywords: Abstract Control Stacks, COMPSAC 2009, IR Programs, Modular Certification, Software Engineering