Name
Abstract | ||
|---|---|---|
Abstract Garbage-collected languages,such as Java and C# are becoming more,and more,widely used in both high-end software and realtime embedded,applications. The correctness of the GC implementation is essential to the reliability and security of a large portion of the world’s mission-critical software. Unfortunately, garbage collectorsóespecially incremental and concurrent onesóare,extremely hard to implement correctly. In this paper, we present a new uniform,approach,to verifying the safety of both a mutator and its garbage collector in Hoare-style logic. We dene,a formal garbage collector interface general enough,to reason about a variety of algorithms while allowing the mutator to ignore implementationspecic,details of the collector. Our approach,supports collectors that require read and write barriers. We have used our approach to mechanically verify assembly implementations of mark-sweep, copying and incremental copying GCs in Coq, as well as sample mutator programs that can be linked with any of the GCs to produce a fully-veried,garbage-collected program. Our work provides a foundation for reasoning about complex mutator-collector interaction and makes an important advance toward building fully certied production-quality GCs. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; D.2.4 [Software Engineering]: Software/Program Verication ó correctness proofs, formal methods General Terms Languages, Verication Keywords Garbage Collection, Abstract Data Type, Assembly |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1273442.1250788 | SIGPLAN Conference on Programming Language Design and Implementation |
Keywords | Field | DocType |
new uniform approach,certifying garbage collector,assembly code verification,gc implementation,formal garbage collector interface,production-quality gcs,general framework,proof-carrying code,garbage-collected language,garbage collector,incremental copying gcs,mission-critical software,abstract data type,separation logic,high-end software,garbage collection,sample mutator program,software engineering,formal method | Garbage,Separation logic,Programming language,Computer science,Correctness,Hoare logic,Real-time computing,Proof-carrying code,Garbage collection,Garbage in, garbage out,Java | Conference |
Volume | Issue | ISSN |
42 | 6 | 0362-1340 |
Citations | PageRank | References |
38 | 1.64 | 32 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrew McCreight | 1 | 75 | 4.15 |
| Zhong Shao | 2 | 897 | 68.80 |
| Chunxiao Lin | 3 | 52 | 3.78 |
| Long Li | 4 | 38 | 1.64 |