Virtual machines for JavaScript, Flash ActionScript, Java, and C# rely on garbage collection to safely remove unreachable objects from memory. Unfortunately, bugs in garbage collector implementations have often undermined this safety, causing security vulnerabilities in several popular web browsers over the past two years. To prevent such vulnerabilities, it's useful to verify that garbage collectors work correctly. We describe how we used the Boogie verification condition generator and Z3 automated theorem prover to prove the partial correctness of two practical garbage collectors (one mark-sweep collector and one copying collector). Our work leverages recent advances in automated theorem proving technology, using Z3's support for arithmetic, arrays, and bit vectors to reason about the low-level details of memory layout. This low level of detail allowed us to verify not just the GC algorithm, but also the GC interface to real x86 code compiled from off-the-shelf C# programs.