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.
- Akash Lal and Shaz Qadeer, Applying SMT-Based Verification to Device Drivers (Powering the Static Driver Verifier using Corral), in Foundations of Software Engineering (FSE), November 2014
- Akash Lal and Shaz Qadeer, Reachability Modulo Theories, in 7th International workshop on Reachability Problems (Invited Paper), September 2013
- Michael Emmi, Akash Lal, and Shaz Qadeer, Asynchronous programs with prioritized task buffers, in Foundations of Software Engineering (FSE), November 2012
- Michael Emmi and Akash Lal, Finding Non-Terminating Executions in Distributed Asynchronous Programs, in Static Analysis Symposium (SAS), September 2012
- 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
- Michael Emmi, Akash Lal, and Shaz Qadeer, Asynchronous programs with prioritized task buffers, no. MSR-TR-2012-1, January 2012
- Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012
- Prathmesh Prabhu, Thomas Reps, Akash Lal, and Nicholas Kidd, Verifying Concurrent Programs via Bounded Context-Switching and Induction , November 2011
- Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric, Delay-bounded scheduling, in Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Association for Computing Machinery, Inc., January 2011
- Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric, Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers, in Computer Aided Verification (CAV '09), Springer Verlag, February 2009
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]
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)