Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
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

    2013

    2010

    2009

    2008

    2007

    2006

    Download

    A download is available here.

     

    Interns

    2008

    2007

    2006