| Verification of an Incremental Garbage Collector in Hoare-Style Logic |
| Received:August 6,2007 Revised:April 7,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: 719 |
| Download times: 367 |
|
| 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 Fulltext View/Add Comment Download reader |
