Safety Verification of Dynamic Storage Management in Coq

Xiang Sen, Chen Yiyun, Lin Chunxiao, and Li Long

Journal of Computer Research and Development > 2007 > 44(2): 361-367.

Xiang Sen, Chen Yiyun, Lin Chunxiao, and Li Long. Safety Verification of Dynamic Storage Management in Coq[J]. Journal of Computer Research and Development, 2007, 44(2): 361-367.

Citation:

Xiang Sen, Chen Yiyun, Lin Chunxiao, and Li Long. Safety Verification of Dynamic Storage Management in Coq[J]. Journal of Computer Research and Development, 2007, 44(2): 361-367.

Citation:

Xiang Sen, Chen Yiyun, Lin Chunxiao, and Li Long. Safety Verification of Dynamic Storage Management in Coq[J]. Journal of Computer Research and Development, 2007, 44(2): 361-367.

PDF (432 KB)

Safety Verification of Dynamic Storage Management in Coq

Xiang Sen, Chen Yiyun, Lin Chunxiao, and Li Long

(Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230027)

More Information

Published Date: February 14, 2007

Graphical Abstract

Abstract

Abstract

The increasing scale and complexity of software makes the software safety and security critical. Thus more and more research focuses on the development of high-assurance software. Since type system is not expressive enough, the existing research does not touch the verification of infrastructure codes. In this paper, a certified dynamic storage management library is built using Hoare-logic style reasoning at the assembly level with the assistance of a theorem formalization and proof tool called Coq, since Hoare logic is more expressive. This work is a significant application of program verification technique. The experiment shows that program verification can be applied in high-assurance software development.
- formal method,
- high-assurance software,
- program verification,
- proof carrying code

FullText(HTML)

References (0)

[1]	Hu Yujing, Gao Yang, An Bo. Online Counterfactual Regret Minimization in Repeated Imperfect Information Extensive Games[J]. Journal of Computer Research and Development, 2014, 51(10): 2160-2170. DOI: 10.7544/issn1000-1239.2014.20130823
[2]	Tian Youliang, Peng Chenggen, Ma Jianfeng, Jiang Qi, Zhu Jianming. Game-Theoretic Mechanism for Cryptographic Protocol[J]. Journal of Computer Research and Development, 2014, 51(2): 344-352.
[3]	Zhu Guiming, Jin Shiyao, Guo Deke, Wei Hailiang. SOSC：A Self-Organizing Semantic Cluster Based P2P Query Routing Algorithm[J]. Journal of Computer Research and Development, 2011, 48(5): 736-745.
[4]	Cheng Bailiang, Zeng Guosun, Jie Anquan. Study of Multi-Agent Trust Coalition Based on Self-Organization Evolution[J]. Journal of Computer Research and Development, 2010, 47(8): 1382-1391.
[5]	Shi Chunqi, Shi Zhiping, Liu Xi, Shi Zhongzhi. Image Segmentation Based on Self-Organizing Dynamic Neural Network[J]. Journal of Computer Research and Development, 2009, 46(1): 23-30.
[6]	Luo Junhai and Fan Mingyu. Research on Trust Model Based on Game Theory in Mobile Ad-Hoc Networks[J]. Journal of Computer Research and Development, 2008, 45(10): 1704-1710.
[7]	Wang Wei and Zeng Guosun. Self-Organization Resource Topology Revolution Based on Trust Mechanism[J]. Journal of Computer Research and Development, 2007, 44(11): 1849-1856.
[8]	Huang Guanyao, Hong Peilin, and Li Jinsheng. P2P-VCG: A Game Theory Proposal for Bandwidth Allocation[J]. Journal of Computer Research and Development, 2007, 44(1): 78-84.
[9]	Tang Jiuyang, Zhang Weiming, Xiao Weidong, and Tang Daquan. Self-Organizing Peer-to-Peer Network Based on Community Mimicking Social Society[J]. Journal of Computer Research and Development, 2006, 43(8): 1383-1390.
[10]	Hou Yuexian, Ding Zheng, and He Pilian. Self-Organizing Isometric Embedding[J]. Journal of Computer Research and Development, 2005, 42(2): 188-195.