Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor.

Kayvan Memarian, Ben Simner, David Kaloper-Mersinjak, Thibaut Prami, Peter Sewell

Browse the full SOSP paper archive.