{"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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/boogie-org\/boogie\">Boogie <span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/boogie-org\/corral\">GitHub<span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/boogie-org\/sdvbench\">Microsoft Static Driver Verifier Benchmarks<span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/msdn.microsoft.com\/en-us\/library\/windows\/hardware\/ff552808(v=vs.85).aspx\">Static Driver Verifier <span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/boogie-org\/bytecodetranslator\">The Bytecode Translator <span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/smackers\/smack\">SMACK<span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/martinschaef\/jar2bpl\">Jar2bpl<span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/sv-comp.sosy-lab.org\/2017\/results\/results-verified\/\">won second place <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>at the Software Verification Competition <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/sv-comp.sosy-lab.org\/2017\/\">SV-COMP 2017<span class=\"sr-only\"> (opens in new tab)<\/span><\/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<div data-wp-context='{\"items\":[]}' data-wp-interactive=\"msr\/accordion\">\n\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t<div\n\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t>\n\t\t\t\t\t<button\n\t\t\t\t\t\tclass=\"btn btn-link m-0\"\n\t\t\t\t\t\tdata-bi-cN=\"Expand all\"\n\t\t\t\t\t\tdata-wp-bind--aria-controls=\"state.ariaControls\"\n\t\t\t\t\t\tdata-wp-bind--aria-expanded=\"state.ariaExpanded\"\n\t\t\t\t\t\tdata-wp-bind--disabled=\"state.isAllExpanded\"\n\t\t\t\t\t\tdata-wp-class--inactive=\"state.isAllExpanded\"\n\t\t\t\t\t\tdata-wp-on--click=\"actions.onExpandAll\"\n\t\t\t\t\t\ttype=\"button\"\n\t\t\t\t\t>\n\t\t\t\t\t\tExpand all\t\t\t\t\t<\/button>\n\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t<button\n\t\t\t\t\t\tclass=\"btn btn-link m-0\"\n\t\t\t\t\t\tdata-bi-cN=\"Collapse all\"\n\t\t\t\t\t\tdata-wp-bind--aria-controls=\"state.ariaControls\"\n\t\t\t\t\t\tdata-wp-bind--aria-expanded=\"state.ariaExpanded\"\n\t\t\t\t\t\tdata-wp-bind--disabled=\"state.isAllCollapsed\"\n\t\t\t\t\t\tdata-wp-class--inactive=\"state.isAllCollapsed\"\n\t\t\t\t\t\tdata-wp-on--click=\"actions.onCollapseAll\"\n\t\t\t\t\t\ttype=\"button\"\n\t\t\t\t\t>\n\t\t\t\t\t\tCollapse all\t\t\t\t\t<\/button>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t\t\t<ul class=\"msr-accordion\">\n\t\t\t\t\t\t\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-2\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-2\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-1\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tExternal Collaborators\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-1\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-2\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\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=\"_blank\" rel=\"noopener noreferrer\"><img decoding=\"async\" id=\"Image92fc1781-14f1-4c16-b6d7-f6cf76bc8c67\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verifierq-mje-photo9.jpg\" \/><span class=\"sr-only\"> (opens in new tab)<\/span><\/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=\"_blank\" rel=\"noopener noreferrer\"><img decoding=\"async\" id=\"Image24905621-654a-4832-bd53-8961dcf94a34\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verifierq-zvonimir_rakamaric.jpg\" \/><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><span id=\"ImageCaption24905621-654a-4832-bd53-8961dcf94a34\" class=\"ImageCaptionCoreCss ImageCaption\">Z. Rakamaric<\/span><\/span><\/p>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-4\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-4\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-3\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tCorral in Action\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-3\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-4\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\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=\"_blank\" rel=\"noopener noreferrer\">link<span class=\"sr-only\"> (opens in new tab)<\/span><\/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=\"_blank\" rel=\"noopener noreferrer\">link<span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.cs.ox.ac.uk\/people\/vincent.nimal\/cav12\/\">website<span class=\"sr-only\"> (opens in new tab)<\/span><\/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\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/users.ecs.soton.ac.uk\/gp4\/papers\/CAV2011.pdf\">paper<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/users.ecs.soton.ac.uk\/gp4\/papers\/CAV2011experiments.html\">experiments<span class=\"sr-only\"> (opens in new tab)<\/span><\/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<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t\t\t\t\t<\/ul>\n\t<\/div>\n\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,"_classifai_error":"","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":[166835,674928,674385,418112,267396,238171,168251,167962,167947,167016,157365,165218,162941,162528,162171,161859,161858,161273,160467],"related-downloads":[],"related-videos":[695958,695964],"related-groups":[144812,144939],"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","targetHints":{"allow":["GET"]}}],"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}]}}