Local Verification of Global Invariants in Concurrent Programs

We describe a practical method for reasoning about realistic concurrent programs. Our method allows global two-state invariants that restrict update of shared state. We provide simple, sufficient conditions for checking those global invariants modularly. The method has been implemented in VCC3 , an automatic, sound, modular verifier for concurrent C programs. VCC has been used to verify functional correctness of tens of thousands of lines of Microsoft's Hyper-V virtualization platform4 and of SYSGO's embedded real-time operating system PikeOS.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies
• Keywords: CAV 2010, Global Two-state Invariants, Hardware, Practical Method, Realistic Concurrent Programs