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.
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.
- Best Paper Award, Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost, FMCAD 2020.
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.
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.
Corral in Action
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]
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)
Senior Principal Researcher
Senior Principal Researcher