Loading...
Please wait, while we are loading the content...
Similar Documents
A Mechanized Refinement Proof for a Garbage Collector
| Content Provider | Semantic Scholar |
|---|---|
| Author | Havelund, Klaus Shankar, Natarajan |
| Copyright Year | 1997 |
| Abstract | We describe how the PVS veri cation system has been used to verify a safety property of a garbage collection algorithm. The safety property basically says that \nothing but garbage is ever collected". The proof is based on re nement mappings as suggested by Lamport. Although the algorithm is relatively simple, its parallel composition with a \user" program that (nearly) arbitrarily modi es the memory makes the veri cation quite challenging. The garbage collection algorithm and its composition with the user program is regarded as a concurrent system with two processes working on a shared memory. Such concurrent systems can be encoded in PVS as state transition systems, very similar to the model of, for example, TLA. The safety proof is formulated as a re nement, where the safety speci cation itself is formulated as state transition system and where the nal algorithm is shown to be a re nement thereof. The algorithm is an excellent test-case for formal methods, be they based on theorem proving or model checking. Various hand-written proofs of the algorithm have been developed, some of which are wrong. David Russino has veri ed the algorithm in the BoyerMoore prover, but his proof is not based on re nement, implying that his safety property cannot be appreciated without a glass box view of the algorithm, considering it's internal structure. Using re nement, however, the algorithm can be regarded as a black box. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.havelund.com/Publications/gc-refine-report.pdf |
| Alternate Webpage(s) | http://ase.arc.nasa.gov/havelund/Publications/gc-paper.ps.Z |
| Alternate Webpage(s) | http://ase.arc.nasa.gov/havelund/Publications/gc-refine-report.ps.Z |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
