Sciweavers

Share
COMPSAC
2009
IEEE

Modular Certification of Low-Level Intermediate Representation Programs

8 years 11 months ago
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...
Yuan Dong, Shengyuan Wang, Liwei Zhang, Ping Yang
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2009
Where COMPSAC
Authors Yuan Dong, Shengyuan Wang, Liwei Zhang, Ping Yang
Comments (0)
books