{"id":337895,"date":"2016-12-18T16:47:41","date_gmt":"2016-12-19T00:47:41","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=337895"},"modified":"2018-10-16T20:17:04","modified_gmt":"2018-10-17T03:17:04","slug":"thread-modular-abstraction-refinement","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/thread-modular-abstraction-refinement\/","title":{"rendered":"Thread-modular abstraction refinement"},"content":{"rendered":"
\n

We present an algorithm called Tar<\/span> (\u201cThread-modular Abstraction Refinement\u201d) for model checking safety properties of concurrent software. The Tar<\/span> algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that Tar<\/span> explores the state space of one thread at a time, making assumptions about how the environment can interfere. The Tar<\/span>algorithm uses counterexample-guided predicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at the same time environment assumptions are approximated from below. In our software verification tool Blast<\/span> we have implemented a fully automatic race checker for multithreaded C programs which is based on the Tar<\/span> algorithm. This tool has verified a wide variety of commonly used locking idioms, including locking schemes that are not amenable to existing dynamic and static race checkers such as Eraser<\/span> or Warlock<\/span>.<\/p>\n<\/section>\n","protected":false},"excerpt":{"rendered":"

We present an algorithm called Tar (\u201cThread-modular Abstraction Refinement\u201d) for model checking safety properties of concurrent software. The Tar algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that Tar explores the state space of one thread at a time, making assumptions about how […]<\/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 Berlin Heidelberg","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"Proceedings of the International Conference on Computer-Aided Verification","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"","msr_page_range_start":"","msr_page_range_end":"","msr_series":"","msr_volume":"","msr_copyright":"","msr_conference_name":"Proceedings of the International Conference on Computer-Aided Verification","msr_doi":"10.1007\/978-3-540-45069-6_27","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":"2003-07-08","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"http:\/\/link.springer.com\/chapter\/10.1007%2F978-3-540-45069-6_27","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":[13561],"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-337895","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-algorithms","msr-locale-en_us"],"msr_publishername":"Springer Berlin Heidelberg","msr_edition":"Proceedings of the International Conference on Computer-Aided Verification","msr_affiliation":"","msr_published_date":"2003-07-08","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","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:\/\/link.springer.com\/chapter\/10.1007%2F978-3-540-45069-6_27","msr_doi":"10.1007\/978-3-540-45069-6_27","msr_publication_uploader":[{"type":"url","title":"http:\/\/link.springer.com\/chapter\/10.1007%2F978-3-540-45069-6_27","viewUrl":false,"id":false,"label_id":0},{"type":"doi","title":"10.1007\/978-3-540-45069-6_27","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:\/\/link.springer.com\/chapter\/10.1007%2F978-3-540-45069-6_27"}],"msr-author-ordering":[{"type":"text","value":"Thomas A. Henzinger","user_id":0,"rest_url":false},{"type":"text","value":"Ranjit Jhala","user_id":0,"rest_url":false},{"type":"text","value":"Rupak Majumdar","user_id":0,"rest_url":false},{"type":"user_nicename","value":"qadeer","user_id":33294,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=qadeer"}],"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\/337895","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":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/337895\/revisions"}],"predecessor-version":[{"id":526141,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/337895\/revisions\/526141"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=337895"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=337895"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=337895"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=337895"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=337895"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=337895"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=337895"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=337895"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=337895"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=337895"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=337895"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=337895"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=337895"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}