Verification of an Incremental Garbage Collector in Hoare-Style Logic
Received:August 06, 2007  Revised:April 07, 2009  Download PDF
Chunxiao Lin,Yiyun Chen,and Bei Hua. Verification of an Incremental Garbage Collector in Hoare-Style Logic. International Journal of Software and Informatics, 2009,3(1):67~88
Hits: 3596
Download times: 2459
Fund:This work is sponsored by the National Natural Science Foundation of China under Grant Nos.90718026 and 60673126 and Intel China Research Center
Abstract:Many of the current software systems rely on garbage collectors for automatic memory management. This is also the case for various software systems in real-time appli-cations. However, a real-time application often requires an incremental working style of the underlying garbage collection, which renders the garbage collector more complex and less trustworthy. We present a formal veriˉcation of the Yuasa incremental garbage collector in Hoare-style logic. The speciˉcation and proof of the collector are built on a concrete machine model and cover detailed behaviors of the collector which may lead to safety prob- lems but are often ignored in high-level veriˉcations. The work is fully implemented with the Coq proof assistant and can be packed as foundational proof-carrying-code packages.Our work makes an important step toward providing high-assurance garbage collection for mission-critical real-time systems.
keywords:program verification  incremental garbage collector  separation logic  proofcarrying code
View Full Text  View/Add Comment  Download reader



Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号