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.
• 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.

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.