Computer Science – Programming Languages
Scientific paper
2010-04-21
LMCS 6 (3:6) 2010
Computer Science
Programming Languages
Scientific paper
10.2168/LMCS-6(3:6)2010
Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the proofs were hand-written or the collectors were too simplistic to use on practical applications. In this work, we present two mechanically verified garbage collectors, both practical enough to use for real-world C# benchmarks. The collectors and their associated allocators consist of x86 assembly language instructions and macro instructions, annotated with preconditions, postconditions, invariants, and assertions. We used the Boogie verification generator and the Z3 automated theorem prover to verify this assembly language code mechanically. We provide measurements comparing the performance of the verified collector with that of the standard Bartok collectors on off-the-shelf C# benchmarks, demonstrating their competitiveness.
Hawblitzel Chris
Petrank Erez
No associations
LandOfFree
Automated Verification of Practical Garbage Collectors does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Automated Verification of Practical Garbage Collectors, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automated Verification of Practical Garbage Collectors will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-458547