HAVOC
HAVOC is a tool for specifying and checking properties of systems software written in 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 rich properties about the program heap and data structures such as linked lists and arrays.
Publications
2009
- Shuvendu K. Lahiri and Shaz Qadeer, Complexity and algorithms for monomial and clausal predicate abstraction, in International Conference on Automated Deduction (CADE '09), Springer Verlag, March 2009
- Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric, Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers, in Computer Aided Verification (CAV '09), Springer Verlag, February 2009
- Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, and Thomas Wies, Intra-Module Inference, in Computer Aided Verification (CAV '09), Springer Verlag, February 2009
- Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, and Shaz Qadeer, Unifying Type Checking and Property Checking for Low-Level Code, in Principles of Programming Languages (POPL '09), Association for Computing Machinery, Inc., January 2009
2008
- Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, and Thomas Ball, Scalable Modular Checking of System-Specific Properties: Myth or Reality?, no. MSR-TR-2008-82, May 2008
- Shuvendu Lahiri and Shaz Qadeer, Back to the Future: Revisiting Precise Program Verification using SMT Solvers, in Principles of Programming Languages (POPL '08), Association for Computing Machinery, Inc., January 2008
2007
- Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, and Zvonimir Rakamaric, A Reachability Predicate for Analyzing Low-Level Software, in Tools and Algorithms for the Construction and Analysis of Systems (TACAS '07), Springer Verlag, April 2007
2006
- Shuvendu K. Lahiri and Shaz Qadeer, Verifying properties of well-founded linked lists, in Principles of Programming Languages (POPL '06), ACM, 2006
