Automated Verification of Practical Garbage Collectors - Computer Science > Programming LanguagesReport as inadecuate




Automated Verification of Practical Garbage Collectors - Computer Science > Programming Languages - Download this document for free, or read online. Document in PDF available to download.

Abstract: Garbage collectors are notoriously hard to verify, due to their low-levelinteraction with the underlying system and the general difficulty in reasoningabout reachability in graphs. Several papers have presented verifiedcollectors, but either the proofs were hand-written or the collectors were toosimplistic to use on practical applications. In this work, we present twomechanically verified garbage collectors, both practical enough to use forreal-world C# benchmarks. The collectors and their associated allocatorsconsist of x86 assembly language instructions and macro instructions, annotatedwith preconditions, postconditions, invariants, and assertions. We used theBoogie verification generator and the Z3 automated theorem prover to verifythis assembly language code mechanically. We provide measurements comparing theperformance of the verified collector with that of the standard Bartokcollectors on off-the-shelf C# benchmarks, demonstrating their competitiveness.



Author: Chris Hawblitzel Microsoft, Erez Petrank Technion

Source: https://arxiv.org/







Related documents