@techreport{moskal2009a,
author = {Moskal, Michal and Schulte, Wolfram and Cohen, Ernie and Tobies, Stephan},
title = {A Practical Verification Methodology for Concurrent Programs},
year = {2009},
month = {February},
abstract = {We describe a methodology for reasoning about realistic concurrent programs. Our methodology allows two-state invariants that span multiple objects without sacrificing thread- or data-modularity, as well as the derived construction of first-class objects that capture knowledge about the system state. The methodology has been implemented in an automatic sound verifier for concurrent C programs being used to verify the code of the Microsoft Hypervisor, the virtualization kernel of Hyper-V.},
publisher = {Microsoft},
url = {http://approjects.co.za/?big=en-us/research/publication/a-practical-verification-methodology-for-concurrent-programs/},
number = {MSR-TR-2009-2019},
}