Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Q Program Verifier

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.

External Collaborators

Mike Emmi                   Z. Rakamaric

Publications

Links

Q 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]

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)