Trace Id is missing

Unlock your potential with Microsoft Copilot

Get things done faster and unleash your creativity with the power of AI anywhere you go.
Microsoft Copilot app being utilized to generate pictures of a singing dog, assisting to identify a flower, and helping to generate an email to congratulate a coworker on a promotion.

HAVOC: Heap-Aware Verifier for C Programs

HAVOC is a modular verifier for systems software written in C. Last published: June 2, 2008.

Important! Selecting a language below will dynamically change the complete page content to that language.

Download
  • Version:

    0.1

    Date Published:

    5/12/2016

    File Name:

    havoc_v_0.1_external_setup.msi

    File Size:

    9.6 MB

    HAVOC is a modular verifier for systems software written in C. It takes as input an annotated C program, in the form of pre- and post-conditions and loop invariants, and uses the Boogie verifier and the SMT solver Z3 to check the annotations. The novelty of the tool lies in a) an accurate memory model for C accounting for low-level operations such as pointer arithmetic, address-of operations, and casts; b) an expressive annotation language; and c) efficient decision procedures to reason about the annotations. The annotation language not only supports writing most pointer expressions, but also enables a user to refer to sets of pointers and to express quantified invariants over such sets. We provide support for constructing sets of pointers in a linked list, all indices in an array, and all objects of a given runtime type.
  • Supported Operating Systems

    Windows 10, Windows 7, Windows 8

    • Windows 7, Windows 8, or Windows 10
    • Click Download and follow the instructions.
Follow Microsoft