HAVOC is a tool for specifying and checking properties of systems software written in C, similar in spirit to the Spec# effort for C#. The tool understands low-level pointer manipulations, internal pointers, and cast operations that are prevalent in systems software. The annotation language of HAVOC allows the expression of richer properties about the program heap and data structures such as linked lists and arrays. HAVOC is a modular verifier. The user provides annotates the program with specifications and HAVOC checks the annotated program modularly, one procedure at a time, using an automated theorem prover. Currently, we are using HAVOC to specify and check complex locking protocols over heap-allocated data structures in Windows, properties of collections such as IRP queues in device drivers, and correctness properties of custom storage allocators.

HAVOC version 0.1 is available for download from here!!

Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer
Microsoft Research Technical Report MSR-TR-2008-96, July 2008

Annotation-based property checking for systems software
Thomas Ball, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer
Microsoft Research Technical Report MSR-TR-2008-82, May 2008

Back to the Future: Revisiting Precise Program Verification using SMT Solvers
Shuvendu K. Lahiri and Shaz Qadeer
In Proceedings of the 35th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, 2008.
(Preliminary) Microsoft Research Technical Report MSR-TR-2007-88, July 2007
[Benchmarks]

A Reachability Predicate for Analyzing Low-Level Software
Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer and Zvonimir Rakamaric.
In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2007
[Benchmarks]

Verifying Properties of Well-Founded Linked Lists.
Shuvendu K. Lahiri and Shaz Qadeer.
Microsoft Research Technical Report MSR-TR-2005-97, July 2005.
In Proceedings of the 33rd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, 2006.

• Jeremy Condit
• Shuvendu Lahiri
• Shaz Qadeer

Summer interns 2008:

• Juan Pablo Galeotti, University of Buenos Aires
• Jan Wen Voung, University of California, San Diego

Summer interns 2007:

• Thomas Wies, University of Freiburg
• Brian Hackett, Stanford University
• Ian Wehrman, University of Texas at Austin

(Past) summer interns:

• Zvonimir Rakamaric, University of British Columbia
• Shaunak Chatterjee, Indian Institute of Technology Kharagpur