{"id":170110,"date":"2008-12-10T11:07:20","date_gmt":"2008-12-10T11:07:20","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/vcc-a-verifier-for-concurrent-c\/"},"modified":"2018-04-03T16:39:58","modified_gmt":"2018-04-03T23:39:58","slug":"vcc-a-verifier-for-concurrent-c","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/vcc-a-verifier-for-concurrent-c\/","title":{"rendered":"VCC: A Verifier for Concurrent C"},"content":{"rendered":"<p class=\"asset-content\"><span id=\"cf640d4c-72b8-45e7-9a6f-ae11b9310243\" class=\"ImageBlock fl\"><img decoding=\"async\" id=\"Imagecf640d4c-72b8-45e7-9a6f-ae11b9310243\" class=\"alignleft\" title=\"VCC Logo\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/vcc-vcc-150x139.png\" alt=\"VCC Logo\" \/><span id=\"ImageCaptioncf640d4c-72b8-45e7-9a6f-ae11b9310243\" class=\"ImageCaptionCoreCss ImageCaption\"><\/span><\/span>VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity.<\/p>\n<div id=\"en-usprojectsvccdefault\" class=\"page-content\">\n<p>VCC is available for non-commercial use, with sources, at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/vcc.codeplex.com\/\">our codeplex site<\/a>.<\/p>\n<\/div>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<div id=\"en-usprojectsvccdefault\" class=\"page-content\">\n<h1>Workflow<\/h1>\n<p>The work flow is illustrated by the figure below. One starts with annotating the C code with contracts. Contracts are written using C preprocessor macros, so one can get rid of them using a single preprocessor switch and compile the code using one&#8217;s favorite C compiler. If the contracts are left in place, VCC when run on a program will report:<\/p>\n<ul>\n<li>that the program is correct, in which case we&#8217;re happy<\/li>\n<li>that an assertion might fail during execution of the program, in which case we can use <b>Model Viewer<\/b> (another tool developed withing the VCC project) application to inspect the circumstances in which the assertion might fail<\/li>\n<li>the prover will diverge&#8211;it&#8217;s unfortunately the case that verification is undecidable&#8211;in which case we can see how did the proof go using the <b>Z3\u00a0Axiom Profiler<\/b>\u00a0(formerly Z3 Visualizer, yet another VCC project tool), and perhaps make the specification more bearable to the prover<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<\/div>\n<div id=\"en-usprojectsvccdefault\" class=\"page-content\"><span id=\"50861bdb-0e5e-4b9a-95bb-75ff3f8160ad\" class=\"ImageBlock fn\"><img decoding=\"async\" id=\"Image50861bdb-0e5e-4b9a-95bb-75ff3f8160ad\" title=\"VCC workflow\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/vcc-vccworkflow.png\" alt=\"VCC workflow\" \/><span id=\"ImageCaption50861bdb-0e5e-4b9a-95bb-75ff3f8160ad\" class=\"ImageCaptionCoreCss ImageCaption\"><\/span><\/span><\/div>\n<div id=\"en-usprojectsvccdefault\" class=\"page-content\">\n<p>The VCC research project is being developed primarily in <a href=\"http:\/\/www.microsoft.com\/emic\/default.mspx\">European Microsoft Innovation Center<\/a> in Aachen, Germany and in the <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/group\/rise-working-group-on-program-analysis\/\">RiSE<\/a> group at <a href=\"https:\/\/www.microsoft.com\/en-us\/research\">Microsoft Research<\/a> in Redmond.<\/p>\n<\/div>\n<div id=\"en-usprojectsvccdefault\" class=\"page-content\">\n<h1>Hyper-V<\/h1>\n<p>The current primary goal of the VCC project is to to verify <a href=\"http:\/\/www.microsoft.com\/servers\/hyper-v-server\/default.mspx\">Microsoft Hyper-V<\/a>. The Microsoft Hyper-V is a hypervisor &#8212; a thin layer of software that sits just above the hardware and beneath one or more operating systems. Its primary job is to provide isolated execution environments called partitions. Each partition is provided with its own set of hardware resources (memory, devices, CPU cycles). A hypervisor is responsible for controlling and arbitrating access to the underlying hardware and in particular for maintaining strong isolation between partitions.<\/p>\n<p>Hyper-V consists of about 60 thousand lines of operating system-level C and x64 assembly code, it is therefore not a trivial target.<\/p>\n<h1>Features<\/h1>\n<ul>\n<li><b>soundness<\/b> &#8212; we are aiming at verification of deep system properties, not bug-finding<\/li>\n<li>support for <b>concurrency<\/b> &#8212; operating systems stopped to be single-threaded 20 years ago<\/li>\n<li><b>modularity<\/b> &#8212; swallowing tens of thousands of lines in one chunk might be hard<\/li>\n<li>support for <b>low-level C features<\/b> (bitfields, unions, wrap-around arithmetic) &#8212; we are verifying operating systems after all!<\/li>\n<\/ul>\n<h1>Downloads<\/h1>\n<p>VCC is available for non-commercial use, with sources, at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/vcc.codeplex.com\/\" target=\"_self\">our codeplex site<\/a>.<\/p>\n<\/div>\n<div id=\"en-usprojectsvccdefault\" class=\"page-content\">\n<h1>Talks<\/h1>\n<p>There are also some slide decks from talks:<\/p>\n<ul>\n<li><b>Verifying concurrent C programs with VCC, Boogie and Z3<\/b>. Workshop on Linking Tools for Verified Software, Microsoft Research Cambridge, November 27-28, 2008. Slides as available as\u00a0<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/vcc-vcc-msrc-2008-full.pptx\" target=\"_self\">PPT<\/a>\u00a0or <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/vcc-vcc-msrc-2008-full.pdf\" target=\"_self\">PDF<\/a>, but the PDF version doesn&#8217;t\u00a0have inter-slide transitions.<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to [&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-170110","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":"2008-12-10","related-publications":[158873,155689,155810,157076,155830,155815,155690],"related-downloads":[235205],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Michal Moskal","user_id":37431,"people_section":"Group 1","alias":"mimoskal"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170110"}],"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":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170110\/revisions"}],"predecessor-version":[{"id":477687,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170110\/revisions\/477687"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170110"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170110"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170110"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170110"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170110"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}