Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
A Practical Verification Methodology for Concurrent Programs

Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies

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.

Details

Publication typeTechReport
NumberMSR-TR-2009-2019
PublisherMicrosoft
> Publications > A Practical Verification Methodology for Concurrent Programs