{"id":171153,"date":"2013-05-19T09:16:29","date_gmt":"2013-05-19T09:16:29","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/q-program-verifier\/"},"modified":"2020-10-04T23:48:07","modified_gmt":"2020-10-05T06:48:07","slug":"q-program-verifier","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/q-program-verifier\/","title":{"rendered":"Corral Program Verifier"},"content":{"rendered":"<p>Corral is a\u00a0whole-program analysis tool for <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/boogie-org\/boogie\">Boogie <\/a>programs. Corral uses goal-directed symbolic search techniques to find assertion violations.\u00a0It leverages the powerful\u00a0theorem prover Z3. It is available open source on\u00a0<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/boogie-org\/corral\">GitHub<\/a>.\u00a0Corral, by default, does a bounded search up to a recursion depth and fixed number of context switches. Corral also supports the <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/duality\/\">Duality <\/a>extension for constructing\u00a0inductive proofs of correctness of programs.<\/p>\n<p><strong>New<\/strong>: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/boogie-org\/sdvbench\">Microsoft Static Driver Verifier Benchmarks<\/a><\/p>\n<p><span id=\"06dbac9f-cacc-4cd5-927f-72d0948b1e22\" class=\"ImageBlock fn\"><span id=\"ImageCaption06dbac9f-cacc-4cd5-927f-72d0948b1e22\" class=\"ImageCaptionCoreCss ImageCaption\">Corral powers Microsoft&#8217;s <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/msdn.microsoft.com\/en-us\/library\/windows\/hardware\/ff552808(v=vs.85).aspx\">Static Driver Verifier <\/a>tool. This work has received several best paper awards:<\/span><\/span><\/p>\n<ul>\n<li>ACM SIGSOFT Distinguished Paper Award, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/inferring-annotations-device-drivers-verification-histories-2\/\"><span style=\"color: #0060ac\">Inferring Annotations For Device Drivers From Verification Histories<\/span><\/a>, ASE 2016.<\/li>\n<li>Best Paper Award, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/a-program-transformation-for-faster-goal-directed-search\/\"><span style=\"color: #0060ac\">A Program Transformation for Faster Goal-Directed Search<\/span><\/a>, FMCAD 2014.<\/li>\n<li>ACM SIGSOFT Distinguished Paper Award, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/powering-the-static-driver-verifier-using-corral\/\"><span style=\"color: #0060ac\">Powering the Static Driver Verifier using Corral<\/span><\/a>, FSE 2014.<\/li>\n<li>Best Paper Award, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/angelic-checking-within-static-driver-verifier-towards-high-precision-defects-without-modeling-cost\/\">Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost<\/a>, FMCAD 2020.<\/li>\n<\/ul>\n<p>There are multiple\u00a0front-ends\u00a0that compile source languages to Boogie. These can be paired with Corral to build program verifiers for different languages:<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/boogie-org\/bytecodetranslator\">The Bytecode Translator <\/a>(BCT), for compiling .NET code to Boogie.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/smackers\/smack\">SMACK<\/a>, for compiling C programs to Boogie.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/martinschaef\/jar2bpl\">Jar2bpl<\/a>, for compiling Java programs to Boogie.<\/li>\n<\/ul>\n<p>We\u00a0do not directly support any of these front-ends. Instead, we collaborate with the owners of these projects to make sure\u00a0Corral integrates nicely with these compilers.<\/p>\n<p><strong>News<\/strong>: SMACK, running the Corral verifier <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/sv-comp.sosy-lab.org\/2017\/results\/results-verified\/\">won second place <\/a>at the Software Verification Competition <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/sv-comp.sosy-lab.org\/2017\/\">SV-COMP 2017<\/a>.<\/p>\n<p>Corral used to be paired with <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/havoc\/\">HAVOC<\/a>\u00a0for end-to-end verification of C programs; this combination used to be called &#8220;Poirot&#8221;, but has since gone out of favor due to the effort needed in maintaining a HAVOC version compatible with Corral. Instead, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/smackcorral-a-modular-verifier-competition-contribution\/\">we recommend using <\/a>SMACK for verifying C programs. Please use the name Corral in your research publications from now onwards.<\/p>\n<p>Corral also powers an extension called the\u00a0<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/angelic-verification\/\">Angelic Verifier <\/a>for finding bugs in <em>open<\/em> programs.<\/p>\n<p><strong>Contact:<\/strong> If you are using (or wish to use)\u00a0Corral in your research project, please drop\u00a0an email to the authors listed on this page.<\/p>\n\t\t\t<div class=\"moray-accordion\" data-show=\"false\">\n\t\t\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t\t<div\n\t\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\t\trole=\"group\"\n\t\t\t\t\t\tdata-mount=\"collapse-controls\"\n\t\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t\t\tdata-target=\"#accordion-1\">\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"expand\" type=\"button\" data-bi-cN=\"Expand all\">Expand all<\/button>\n\t\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"collapse\" type=\"button\" data-bi-cN=\"Collapse all\">Collapse all<\/button>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t<ul class=\"accordion\" id=\"accordion-1\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-2\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-2\">\n\t\tExternal Collaborators\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-2\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<h1>External Collaborators<\/h1>\n<p><span id=\"92fc1781-14f1-4c16-b6d7-f6cf76bc8c67\" class=\"ImageBlock fn\"><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.liafa.jussieu.fr\/~mje\/\" target=\"_self\" rel=\"noopener noreferrer\"><img decoding=\"async\" id=\"Image92fc1781-14f1-4c16-b6d7-f6cf76bc8c67\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/verifierq-mje-photo9.jpg\" \/><\/a><span id=\"ImageCaption92fc1781-14f1-4c16-b6d7-f6cf76bc8c67\" class=\"ImageCaptionCoreCss ImageCaption\">Mike Emmi<\/span><\/span>\u00a0\u00a0\u00a0\u00a0 \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 <span id=\"24905621-654a-4832-bd53-8961dcf94a34\" class=\"ImageBlock fn\"><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.zvonimir.info\/\" target=\"_self\" rel=\"noopener noreferrer\"><img decoding=\"async\" id=\"Image24905621-654a-4832-bd53-8961dcf94a34\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/verifierq-zvonimir_rakamaric.jpg\" \/><\/a><span id=\"ImageCaption24905621-654a-4832-bd53-8961dcf94a34\" class=\"ImageCaptionCoreCss ImageCaption\">Z. Rakamaric<\/span><\/span><\/p>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-3\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-3\">\n\t\tCorral in Action\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-3\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<h1>Corral\u00a0in Action<\/h1>\n<p>Online services enhanced with Certified Symbolic Transactions [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/sites.google.com\/site\/symbolictransaction\/\" target=\"_self\" rel=\"noopener noreferrer\">link<\/a>] [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/securing-multiparty-online-services-via-certification-of-symbolic-transactions\/\">paper<\/a>]<\/p>\n<p>Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization. R. Wang, Y. Zhou &#8211; in alphabetical order, S. Chen, S. Qadeer, D. Evans, and Y. Gurevich. [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/explicating-sdks-uncovering-assumptions-underlying-secure-authentication-and-authorization-2\/\">link<\/a>]<\/p>\n<p>Efficient Synthesis for Concurrency using Semantics-Preserving Transformations.P. Cerny, T. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach. [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/ecee.colorado.edu\/pavol\/publications\/\" target=\"_self\" rel=\"noopener noreferrer\">link<\/a>]<\/p>\n<p>Sound and Unified Software Verification for Weak Memory Models. [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cs.ox.ac.uk\/people\/vincent.nimal\/cav12\/\">website<\/a>]<\/p>\n<p>Getting Rid of Store-Buffers in the Analysis of Weak Memory Models. G. Parlato, F. Atig, A. Bouajjani. [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/users.ecs.soton.ac.uk\/gp4\/papers\/CAV2011.pdf\">paper<\/a>, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/users.ecs.soton.ac.uk\/gp4\/papers\/CAV2011experiments.html\">experiments<\/a>]<\/p>\n<p>How to Shop for Free Online \u2013 Security Analysis of Cashier-as-a-Service Based Web Stores. R. Wang, S. Chen, X. Wang, S. Qadeer. [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/how-to-shop-for-free-online-security-analysis-of-cashier-as-a-service-based-web-stores\/\">paper<\/a>]<\/p>\n<p>(Please let us know if your work also uses Corral)<\/p>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t\t\t\t<\/ul>\n\t\t<\/div>\n\t\t\n","protected":false},"excerpt":{"rendered":"<p>Corral is a\u00a0whole-program analysis tool for Boogie programs. Corral uses goal-directed symbolic search techniques to find assertion violations.\u00a0It leverages the powerful\u00a0theorem prover Z3. It is available open source on\u00a0GitHub.\u00a0Corral, 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\u00a0inductive proofs [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-171153","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2013-05-09","related-publications":[162171,418112,162528,674385,162941,674928,165218,166835,167016,157365,167947,160467,167962,161273,168251,161858,238171,161859,267396],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Shuvendu Lahiri","user_id":33640,"people_section":"Group 1","alias":"shuvendu"},{"type":"user_nicename","display_name":"Akash Lal","user_id":30905,"people_section":"Group 1","alias":"akashl"}],"msr_research_lab":[199562,199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171153"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":3,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171153\/revisions"}],"predecessor-version":[{"id":695955,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171153\/revisions\/695955"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=171153"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=171153"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=171153"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=171153"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=171153"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}