A pointer logic and certifying compiler |
| |
Authors: | Chen Yiyun Ge Lin Hua Baojian Li Zhaopeng Liu Cheng and Wang Zhifang |
| |
Affiliation: | (1) Department of Computer Science and Technology, University of Science and Technology of China, Hefei, 230027, China |
| |
Abstract: | Proof-Carrying Code brings two big challenges to the research field of programming languages. One is to seek more expressive
logics or type systems to specify or reason about the properties of low-level or high-level programs. The other is to study
the technology of certifying compilation in which the compiler generates proofs for programs with annotations. This paper
presents our progress in the above two aspects. A pointer logic was designed for PointerC (a C-like programming language)
in our research. As an extension of Hoare logic, our pointer logic expresses the change of pointer information for each statement
in its inference rules to support program verification. Meanwhile, based on the ideas from CAP (Certified Assembly Programming)
and SCAP (Stack-based Certified Assembly Programming), a reasoning framework was built to verify the properties of object
code in a Hoare style. And a certifying compiler prototype for PointerC was implemented based on this framework.
The main contribution of this paper is the design of the pointer logic and the implementation of the certifying compiler prototype.
In our certifying compiler, the source language contains rich pointer types and operations and also supports dynamic storage
allocation and deallocation. |
| |
Keywords: | software safety Hoare logic pointer logic Proof-Carrying Code certifying compiler |
本文献已被 万方数据 SpringerLink 等数据库收录! |