{"id":338030,"date":"2016-12-18T20:49:53","date_gmt":"2016-12-19T04:49:53","guid":{"rendered":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/?post_type=msr-research-item&#038;p=338030"},"modified":"2018-10-16T20:17:27","modified_gmt":"2018-10-17T03:17:27","slug":"induction-compositional-model-checking","status":"publish","type":"msr-research-item","link":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/publication\/induction-compositional-model-checking\/","title":{"rendered":"Induction in Compositional Model Checking"},"content":{"rendered":"<p>This paper describes a technique of inductive proof based on model checking. It differs from previous techniques that combine induction and model checking in that the proof is fully mechanically checked and temporal variables (process identifiers, for example) may be natural numbers. To prove \u2200<em class=\"EmphasisTypeItalic \">n<\/em>.<em class=\"EmphasisTypeItalic \">\u03d5<\/em>(<em class=\"EmphasisTypeItalic \">n<\/em>) inductively, the predicate <span id=\"IEq1\" class=\"InlineEquation\"><span id=\"MathJax-Element-1-Frame\" class=\"MathJax\" style=\"border: 0px; font-style: normal; font-variant: inherit; font-weight: normal; font-stretch: inherit; font-size: 13px; line-height: normal; font-family: inherit; margin: 0px; padding: 0px; vertical-align: baseline; outline: 0px; display: inline; text-indent: 0px; text-align: left; text-transform: none; letter-spacing: normal; word-spacing: normal; word-wrap: normal; white-space: nowrap; float: none; direction: ltr; max-width: none; max-height: none; min-width: 0px; min-height: 0px; position: relative;\" tabindex=\"0\" data-mathml=\"<math xmlns=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mi>&#x03C6;<\/mi><mo stretchy=\"false\">(<\/mo><mi>n<\/mi><mo>&#x2212;<\/mo><mn>1<\/mn><mo stretchy=\"false\">)<\/mo><mo stretchy=\"false\">&#x21D2;<\/mo><mi>&#x03C6;<\/mi><mo stretchy=\"false\">(<\/mo><mi>n<\/mi><mo stretchy=\"false\">)<\/mo><\/math>\"><span id=\"MathJax-Span-1\" class=\"math\"><span id=\"MathJax-Span-2\" class=\"mrow\"><span id=\"MathJax-Span-3\" class=\"mi\">\u03c6<\/span><span id=\"MathJax-Span-4\" class=\"mo\">(<\/span><span id=\"MathJax-Span-5\" class=\"mi\">n<\/span><span id=\"MathJax-Span-6\" class=\"mo\">\u2212<\/span><span id=\"MathJax-Span-7\" class=\"mn\">1<\/span><span id=\"MathJax-Span-8\" class=\"mo\">)<\/span><span id=\"MathJax-Span-9\" class=\"mo\">\u21d2<\/span><span id=\"MathJax-Span-10\" class=\"mi\">\u03c6<\/span><span id=\"MathJax-Span-11\" class=\"mo\">(<\/span><span id=\"MathJax-Span-12\" class=\"mi\">n<\/span><span id=\"MathJax-Span-13\" class=\"mo\">)<\/span><\/span><\/span><span class=\"MJX_Assistive_MathML\">\u03c6(n\u22121)\u21d2\u03c6(n)<\/span><\/span><\/span> must be proved for all values of the parameter <em class=\"EmphasisTypeItalic \">n<\/em>. Its proof for a fixed\u00a0<em class=\"EmphasisTypeItalic \">n<\/em> uses a conservative abstraction that partitions the natural numbers into a finite number of intervals. This renders the model finite. Further, the abstractions for different values of <em class=\"EmphasisTypeItalic \">n<\/em> fall into a finite number of isomorphism classes. Thus, an inductive proof of \u2200<em class=\"EmphasisTypeItalic \">n<\/em>.<em class=\"EmphasisTypeItalic \">\u03d5<\/em>(<em class=\"EmphasisTypeItalic \">n<\/em>) can be obtained by checking a finite number of formulas on finite models. The method is integrated with a compositional proof system based on the SMV model checker. It is illustrated by examples, including the <em class=\"EmphasisTypeItalic \">N<\/em>-process \u201cbakery\u201d mutual exclusion algorithm<\/p>\n","protected":false},"excerpt":{"rendered":"<p>This paper describes a technique of inductive proof based on model checking. It differs from previous techniques that combine induction and model checking in that the proof is fully mechanically checked and temporal variables (process identifiers, for example) may be natural numbers. To prove \u2200n.\u03d5(n) inductively, the predicate \u03c6(n\u22121)\u21d2\u03c6(n)\u03c6(n\u22121)\u21d2\u03c6(n) must be proved for all values [&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":"","msr-author-ordering":null,"msr_publishername":"Springer Berlin Heidelberg","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"12th International Conference","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":"12th International Conference","msr_doi":"10.1007\/10722167_25","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":"2000-07-15","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"http:\/\/link.springer.com\/chapter\/10.1007%2F10722167_25","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-338030","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":"12th International Conference","msr_affiliation":"","msr_published_date":"2000-07-15","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%2F10722167_25","msr_doi":"10.1007\/10722167_25","msr_publication_uploader":[{"type":"url","title":"http:\/\/link.springer.com\/chapter\/10.1007%2F10722167_25","viewUrl":false,"id":false,"label_id":0},{"type":"doi","title":"10.1007\/10722167_25","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%2F10722167_25"}],"msr-author-ordering":[{"type":"text","value":"Kenneth L. McMillan","user_id":0,"rest_url":false},{"type":"user_nicename","value":"qadeer","user_id":33294,"rest_url":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=qadeer"},{"type":"text","value":"James B. Saxe","user_id":0,"rest_url":false}],"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:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/338030","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/338030\/revisions"}],"predecessor-version":[{"id":526284,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/338030\/revisions\/526284"}],"wp:attachment":[{"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/media?parent=338030"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=338030"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=338030"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=338030"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=338030"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=338030"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=338030"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=338030"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=338030"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=338030"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=338030"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=338030"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/new-cm-edgedigital.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=338030"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}