HAVOC
HAVOC is a tool for specifying and checking properties of systems software written in C, in the presence of pointer manipulations, unsafe casts and dynamic memory allocation. The assertion logic of HAVOC allows the expression of properties of linked lists and arrays. The main challenge addressed by the tool are (1) tradeoff between expressiveness of the assertion logic and its computational efficiency, (2) generic inference techniques to relieve users of annotation burden for large modules.
Publications
2010
- Thomas Ball, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer, and Julien Vanegue, Towards scalable modular checking of user-defined properties, in Verified Software: Theories, Tools and Experiments (VSTTE 2010), Springer Verlag, August 2010
- Shuvendu K. Lahiri and Julien Vanegue, ExplainHoudini: Making Houdini inference transparent, no. MSR-TR-2010-118, August 2010
2009
- Shuvendu K. Lahiri and Shaz Qadeer, Call invariants, no. MSR-TR-2009-13, July 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
- K. Rustan M. Leino, This is Boogie 2, 24 June 2008
- Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, and Thomas Ball, Towards scalable modular checking of user-defined properties, 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
