{"id":396329,"date":"2017-07-04T15:19:37","date_gmt":"2017-07-04T22:19:37","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=396329"},"modified":"2018-10-16T20:00:23","modified_gmt":"2018-10-17T03:00:23","slug":"cloudsdv-enabling-static-driver-verifier-using-microsoft-azure","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/cloudsdv-enabling-static-driver-verifier-using-microsoft-azure\/","title":{"rendered":"CloudSDV: Enabling Static Driver Verifier using Microsoft Azure"},"content":{"rendered":"
\n
\n
\n
\n
\n

In this paper we describe our experience of enabling Static Driver Verifier to use the Microsoft Azure cloud computing platform. We first describe in detail our architecture and methodology for enabling SDV to operate in the Microsoft Azure cloud. We then present our results of using CloudSDV on single drivers and driver suites using various configurations of the cloud relative to a local machine. Our experiments show that using the cloud, we are able to achieve speedups in excess of 20x, which has enabled us to perform mass scale verification in a matter of hours as opposed to days. Finally, we present a brief discussion about our results and experiences.<\/p>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

In this paper we describe our experience of enabling Static Driver Verifier to use the Microsoft Azure cloud computing platform. We first describe in detail our architecture and methodology for enabling SDV to operate in the Microsoft Azure cloud. We then present our results of using CloudSDV on single drivers and driver suites using various […]<\/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":"","msr-author-ordering":null,"msr_publishername":"Springer-Verlag New York, Inc. New York, NY, USA","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"IFM 2016 Proceedings of the 12th International Conference on Integrated Formal Methods","msr_editors":"","msr_how_published":"","msr_isbn":"978-3-319-33692-3","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"523-536","msr_page_range_start":"523","msr_page_range_end":"536","msr_series":"","msr_volume":"9681","msr_copyright":"","msr_conference_name":"IFM 2016 Proceedings of the 12th International Conference on Integrated Formal Methods","msr_doi":"10.1007\/978-3-319-33693-0_33","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"2016-06-01","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"http:\/\/dl.acm.org\/citation.cfm?id=2991587","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":0,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13563],"msr-publication-type":[193716],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-396329","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-data-platform-analytics","msr-locale-en_us"],"msr_publishername":"Springer-Verlag New York, Inc. New York, NY, USA","msr_edition":"IFM 2016 Proceedings of the 12th International Conference on Integrated Formal Methods","msr_affiliation":"","msr_published_date":"2016-06-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"523-536","msr_chapter":"","msr_isbn":"978-3-319-33692-3","msr_journal":"","msr_volume":"9681","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"","msr_publicationurl":"http:\/\/dl.acm.org\/citation.cfm?id=2991587","msr_doi":"10.1007\/978-3-319-33693-0_33","msr_publication_uploader":[{"type":"url","title":"http:\/\/dl.acm.org\/citation.cfm?id=2991587","viewUrl":false,"id":false,"label_id":0},{"type":"doi","title":"10.1007\/978-3-319-33693-0_33","viewUrl":false,"id":false,"label_id":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[{"id":0,"url":"http:\/\/dl.acm.org\/citation.cfm?id=2991587"}],"msr-author-ordering":[{"type":"user_nicename","value":"rahulku","user_id":36326,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=rahulku"},{"type":"text","value":"Thomas Ball","user_id":0,"rest_url":false},{"type":"text","value":"Jakob Lichtenberg","user_id":0,"rest_url":false},{"type":"text","value":"Nate Deisinger","user_id":0,"rest_url":false},{"type":"text","value":"Apoorv Upreti","user_id":0,"rest_url":false},{"type":"user_nicename","value":"chetanb","user_id":31394,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=chetanb"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","related_content":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/396329","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/396329\/revisions"}],"predecessor-version":[{"id":396335,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/396329\/revisions\/396335"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=396329"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=396329"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=396329"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=396329"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=396329"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=396329"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=396329"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=396329"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=396329"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=396329"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=396329"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=396329"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=396329"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}