Corral: Capturing Concurrency
Corral is a whole-program analysis tool for Boogie programs. Corral uses bounded goal-directed symbolic search techniques to find assertion violations. It leverages the powerful theorem prover Z3.
Corral is open source. You can obtain it from: corral.codeplex.com. See the documentation tab for instructions on how to build and run corral. Please send feedback to verifierq AT microsoft DOT com.
- Akash Lal and Shaz Qadeer, Reachability Modulo Theories, in 7th International workshop on Reachability Problems (Invited Paper), September 2013.
- Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, in Computer-Aided Verification (CAV), July 2012.
- Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, no. MSR-TR-2012-9, January 2012.
- Akash Lal and Thomas Reps, Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis, in Formal Methods in System Design (FMSD), Springer Verlag, 2009.