When & Where: 1:00pm, Wednesday, Nov 19, 2008, Room 500 AKW
Abstract:
Virtual machines for JavaScript, Flash ActionScript, Java, and C# rely on garbage collection to remove unreachable objects from memory. A bug in the garbage collector could undermine the security of the virtual machine, so it's useful to verify that the garbage collector works 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.