{"id":170384,"date":"2010-01-08T23:10:45","date_gmt":"2010-01-08T23:10:45","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/the-verification-corner\/"},"modified":"2019-08-19T18:04:27","modified_gmt":"2019-08-20T01:04:27","slug":"the-verification-corner","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/the-verification-corner\/","title":{"rendered":"The Verification Corner"},"content":{"rendered":"<p><img loading=\"lazy\" decoding=\"async\" class=\"alignnone\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/the-verification-corner-2.png\" alt=\"\" width=\"341\" height=\"308\" \/><\/p>\n<p>The Verification Corner is a video series on YouTube that explains different concepts of software verification.<\/p>\n<p>&nbsp;<\/p>\n<p><strong><span id=\"6729172b-2cea-46a2-9f49-4b2a293e79d9\" class=\"ImageBlock fn\"><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/channel9.msdn.com\/Blogs\/Peli\/The-Verification-Corner-Stepwise-Refinement\" target=\"_blank\" rel=\"noopener noreferrer\"><img decoding=\"async\" id=\"Image6729172b-2cea-46a2-9f49-4b2a293e79d9\" class=\"alignright\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-stewiserefinement_220_ch9.jpg\" alt=\"\" \/><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><span id=\"ImageCaption6729172b-2cea-46a2-9f49-4b2a293e79d9\" class=\"ImageCaptionCoreCss ImageCaption\"><\/span><\/span>Stepwise refinement &#8211; 10\/8\/2010:<\/strong><\/p>\n<p>In this episode, Kuat Yessenov and <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/leino\/\">Rustan Leino<\/a>, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, show how a program can be constructed by <em>stepwise refinement<\/em>.<\/p>\n<ul>\n<li>YouTube <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=5yQxkE9pjIU\" target=\"_blank\" rel=\"noopener noreferrer\">video<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Channel9 <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/channel9.msdn.com\/Blogs\/Peli\/The-Verification-Corner-Stepwise-Refinement\" target=\"_blank\" rel=\"noopener noreferrer\">Movie and Podcasts<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Chalice Sources <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-duplicatesvideo.zip\" target=\"_self\" rel=\"noopener noreferrer\">[zip]<\/a><\/li>\n<\/ul>\n<p><span id=\"da743ae9-e070-4080-b4f3-c097747c0450\" class=\"ImageBlock fn\"><span id=\"ImageCaptionda743ae9-e070-4080-b4f3-c097747c0450\" class=\"ImageCaptionCoreCss ImageCaption\">\u00a0<\/span><\/span><\/p>\n<p><strong><span id=\"da743ae9-e070-4080-b4f3-c097747c0450\" class=\"ImageBlock fn\"><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/channel9.msdn.com\/posts\/Peli\/The-Verification-Corner-Loop-Termination\/\" target=\"_blank\" rel=\"noopener noreferrer\"><img decoding=\"async\" id=\"Imageda743ae9-e070-4080-b4f3-c097747c0450\" class=\"alignright\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-looptermination_320_ch9.png\" alt=\"\" \/><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><span id=\"ImageCaptionda743ae9-e070-4080-b4f3-c097747c0450\" class=\"ImageCaptionCoreCss ImageCaption\"><\/span><\/span>Loop Termination &#8211;\u00a03\/29\/2010:<\/strong><\/p>\n<p>In this episode, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/leino\/\">Rustan Leino<\/a> shows how to prove loop termination. During his demonstration, Rustan presents the theoretical background information necessary to build the proof before modeling it using the <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness\/\">Dafny language<\/a>.<\/p>\n<ul>\n<li>YouTube <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=kbJO-U9Wp-s\" target=\"_blank\" rel=\"noopener noreferrer\">video<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Channel9 <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/channel9.msdn.com\/posts\/Peli\/The-Verification-Corner-Loop-Termination\/\" target=\"_blank\" rel=\"noopener noreferrer\">Movie and Podcasts<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness\/\">Dafny<\/a> demo project <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-terminationdemo.zip\" target=\"_self\" rel=\"noopener noreferrer\">[zip]<\/a><\/li>\n<\/ul>\n<p><span id=\"3bd9031d-902e-4da4-b50a-bb939e97bf55\" class=\"ImageBlock fn\"><span id=\"ImageCaption3bd9031d-902e-4da4-b50a-bb939e97bf55\" class=\"ImageCaptionCoreCss ImageCaption\">\u00a0<\/span><\/span><\/p>\n<p><b><span id=\"3bd9031d-902e-4da4-b50a-bb939e97bf55\" class=\"ImageBlock fn\"><img decoding=\"async\" id=\"Image3bd9031d-902e-4da4-b50a-bb939e97bf55\" class=\"alignright\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-vcchunker.png\" alt=\"\" \/><span id=\"ImageCaption3bd9031d-902e-4da4-b50a-bb939e97bf55\" class=\"ImageCaptionCoreCss ImageCaption\"><\/span><\/span>Specifications in Action &#8211; The\u00a0Chunker\u00a0&#8211; 3\/1\/2010:<\/b><\/p>\n<p>In this episode, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/leino\/\">Rustan Leino <\/a>writes a string chunker using Spec#. He gives a brief overview how one can specify and implement a program while getting the help from the Spec# verifier.<\/p>\n<ul>\n<li>YouTube <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=HOl11mP4V68\" target=\"_blank\" rel=\"noopener noreferrer\">video<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Channel9 <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/channel9.msdn.com\/posts\/Peli\/The-Verification-Corner-Specifications-in-Action-with-SpecSharp\/\" target=\"_blank\" rel=\"noopener noreferrer\">Movie and Podcasts<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/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=\"http:\/\/specsharp.codeplex.com\/\">Spec#<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> Demo project <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-chunker.zip\" target=\"_self\" rel=\"noopener noreferrer\">[.zip]<\/a><\/li>\n<\/ul>\n<p><span id=\"f3dac38d-55f7-4a6b-8e0d-b06586bc2577\" class=\"ImageBlock fn\"><span id=\"ImageCaptionf3dac38d-55f7-4a6b-8e0d-b06586bc2577\" class=\"ImageCaptionCoreCss ImageCaption\">\u00a0<\/span><\/span><\/p>\n<p><strong><span id=\"f3dac38d-55f7-4a6b-8e0d-b06586bc2577\" class=\"ImageBlock fn\"><img decoding=\"async\" id=\"Imagef3dac38d-55f7-4a6b-8e0d-b06586bc2577\" class=\"alignright\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-loopinvariant.png\" alt=\"\" \/><span id=\"ImageCaptionf3dac38d-55f7-4a6b-8e0d-b06586bc2577\" class=\"ImageCaptionCoreCss ImageCaption\"><\/span><\/span>Loop Invariants &#8211; 1\/12\/2010:<\/strong><\/p>\n<p>In this episode, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/leino\/\">Rustan Leino <\/a>talks about Loop Invariants. He gives a brief summary of the theoretical foundations and shows (using a problem to compute cubes) how a program can sometimes be systematically constructed from its specifications.<\/p>\n<ul>\n<li>YouTube <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=spcfzbisBv4\" target=\"_blank\" rel=\"noopener noreferrer\">video<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Channel9 <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/channel9.msdn.com\/posts\/Peli\/The-Verification-Corner-Loop-Invariants\/\" target=\"_blank\" rel=\"noopener noreferrer\">Movie and Podcasts<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Whiteboard Slides<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-loopinvariant.pdf\" target=\"_self\" rel=\"noopener noreferrer\"> [pdf]<\/a> <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-loopinvariant.pptx\" target=\"_self\" rel=\"noopener noreferrer\">[pptx]<\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/specsharp.codeplex.com\/\" target=\"_blank\" rel=\"noopener noreferrer\">Spec#<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> Demo project <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/verificationcorner-loopinvariant.zip\" target=\"_self\" rel=\"noopener noreferrer\">[.zip]<\/a><\/li>\n<\/ul>\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\tEpisodes - Now on YouTube\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<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=fSWZWXx5ixc\" target=\"_blank\" rel=\"noopener noreferrer\">Modeling, refinement, and verification<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> with Jean-Raymond Abrial<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=P2durYFsJSA\" target=\"_blank\" rel=\"noopener noreferrer\">Using ghost variables and lemmas in a program verification<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> with Jason Koenig<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=BLQo5d3hI4M\" target=\"_blank\" rel=\"noopener noreferrer\">Partial solutions, and comprehensions<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> with Rosemary Monahan<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.youtube.com\/watch?v=5yQxkE9pjIU\" target=\"_blank\" rel=\"noopener noreferrer\">Concurrent programming in Chalice<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> with Peter M\u00fcller<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" title=\"\" href=\"http:\/\/www.youtube.com\/watch?v=xg4wZDJuk6o\" target=\"_blank\" rel=\"noopener noreferrer\">10\/8\/2010: Stepwise Refinement<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>\u00a0with Kuat Yessenov<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" title=\"\" href=\"http:\/\/www.youtube.com\/watch?v=kbJO-U9Wp-s\" target=\"_blank\" rel=\"noopener noreferrer\">3\/29\/2010: Loop Termination<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" title=\"\" href=\"http:\/\/www.youtube.com\/watch?v=HOl11mP4V68\" target=\"_blank\" rel=\"noopener noreferrer\">3\/01\/2010: The Spec# Chunker<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" title=\"\" href=\"http:\/\/www.youtube.com\/watch?v=spcfzbisBv4\" target=\"_blank\" rel=\"noopener noreferrer\">1\/12\/2010: Loop Invariants<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\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>The Verification Corner is a video series on YouTube that explains different concepts of software verification. &nbsp; Stepwise refinement &#8211; 10\/8\/2010: In this episode, Kuat Yessenov and Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, show how a program can be constructed by stepwise refinement. YouTube video Channel9 [&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":[13546,13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170384","msr-project","type-msr-project","status-publish","hentry","msr-research-area-computational-sciences-mathematics","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2010-01-08","related-publications":[],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Peli de Halleux","user_id":32253,"people_section":"Group 1","alias":"jhalleux"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170384","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":6,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170384\/revisions"}],"predecessor-version":[{"id":604446,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170384\/revisions\/604446"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170384"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170384"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170384"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170384"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170384"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}