We have applied rsim to verify Optimizations in parallel contexts Loop invariant hoisting, strength reduction and induction variable elimination dead code elimination Fine-grained impl. concurrent objects Lock-coupling list, counters, Treiber's non-blocking stack concurrent GCD algorithm Concurrent garbage collectors A general GC verification framework Hans boehms concurrent GC[Boehm et al. 91We have applied RGSim to verify … • Optimizations in parallel contexts – Loop invariant hoisting, strength reduction and induction variable elimination, dead code elimination, … • Fine-grained impl. & concurrent objects – Lock-coupling list, counters, Treiber’s non-blocking stack, concurrent GCD algorithm, … • Concurrent garbage collectors – A general GC verification framework – Hans Boehm’s concurrent GC [Boehm et al. 91]