Publications
Groups
Overview
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:
- ACM SIGSOFT Distinguished Paper Award, Inferring Annotations For Device Drivers From Verification Histories, ASE 2016.
- Best Paper Award, A Program Transformation for Faster Goal-Directed Search, FMCAD 2014.
- ACM SIGSOFT Distinguished Paper Award, Powering the Static Driver Verifier using Corral, FSE 2014.
There are multiple front-ends that compile source languages to Boogie. These can be paired with Corral to build program verifiers for different languages:
- The Bytecode Translator (BCT), for compiling .NET code to Boogie.
- SMACK, for compiling C programs to Boogie.
- Jar2bpl, for compiling Java programs to Boogie.
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)
