Corral Program Verifier

Established: May 9, 2013

Corral is a whole-program analysis tool for Boogie programs. Corral uses goal-directed symbolic search techniques to find assertion violations. It leverages the powerful theorem prover Z3. It is available open source on GitHub. Corral, by default, does a bounded search up to a recursion depth and fixed number of context switches. Corral also supports the Duality extension for constructing inductive proofs of correctness of programs.

New: Microsoft Static Driver Verifier Benchmarks

Corral powers Microsoft’s Static Driver Verifier tool. This work has received several best paper awards:

There are multiple front-ends that compile source languages to Boogie. These can be paired with Corral to build program verifiers for different languages:

We do not directly support any of these front-ends. Instead, we collaborate with the owners of these projects to make sure Corral integrates nicely with these compilers.

News: SMACK, running the Corral verifier won second place at the Software Verification Competition SV-COMP 2017.

Corral used to be paired with HAVOC for end-to-end verification of C programs; this combination used to be called “Poirot”, but has since gone out of favor due to the effort needed in maintaining a HAVOC version compatible with Corral. Instead, we recommend using SMACK for verifying C programs. Please use the name Corral in your research publications from now onwards.

Corral also powers an extension called the Angelic Verifier for finding bugs in open programs.

Contact: If you are using (or wish to use) Corral in your research project, please drop an email to the authors listed on this page.

  • External Collaborators

    Mike Emmi                   Z. Rakamaric

  • Corral in Action

    Online services enhanced with Certified Symbolic Transactions [link] [paper]

    Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization. R. Wang, Y. Zhou – in alphabetical order, S. Chen, S. Qadeer, D. Evans, and Y. Gurevich. [link]

    Efficient Synthesis for Concurrency using Semantics-Preserving Transformations.P. Cerny, T. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach. [link]

    Sound and Unified Software Verification for Weak Memory Models. [website]

    Getting Rid of Store-Buffers in the Analysis of Weak Memory Models. G. Parlato, F. Atig, A. Bouajjani. [paper, experiments]

    How to Shop for Free Online – Security Analysis of Cashier-as-a-Service Based Web Stores. R. Wang, S. Chen, X. Wang, S. Qadeer. [paper]

    (Please let us know if your work also uses Corral)

People

People

Portrait of Shuvendu Lahiri

Shuvendu Lahiri

Senior Principal Researcher

Portrait of Akash Lal

Akash Lal

Senior Principal Researcher