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

External Collaborators

Mike Emmi                   Z. Rakamaric

Corral in Action

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)