The Q program verifier is a collection of front-ends that compile different source languages to an intermediate representation (IR), and back-ends that perform verification on the IR. Together, Q is a verification platform that hosts multiple tools and technologies for analyzing properties of programs.
Currently Q supports a single back-end, called Corral, which is a whole-program analyzer for Boogie programs. Corral is a goal-directed symbolic exploration engine that explores all executions of a Boogie program, given a bound on the recursion and the number of context-switches (when dealing with concurrent Boogie programs).
There are three separate front-ends (under active development) that compile source languages to Boogie:
- The Bytecode Translator (BCT), for compiling .NET code to Boogie.
- SMACK, for compiling C programs to Boogie.
- Jar2bpl, for compiling Java programs to Boogie.
The Q team does not directly support any of these front-ends. Instead, we collaborate with the owners of these projects to make sure the back-ends (in this case, only Corral) integrate 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 Q or Corral in your research publications from now onwards.
We will soon have Q live on: http://www.rise4fun.com/
Contact: If you are using (or wish to use) Q in your research project, please drop us an email at verifierq at microsoft dot com.
Mike Emmi Z. Rakamaric
Q in Action
Online services enhanced with Certified Symbolic Transactions [link] [paper] New
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 Q)
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.