{"id":19572,"date":"2020-06-29T09:20:52","date_gmt":"2020-06-29T13:20:52","guid":{"rendered":"https:\/\/michigan.it.umich.edu\/news\/?p=19572"},"modified":"2024-07-08T06:04:55","modified_gmt":"2024-07-08T10:04:55","slug":"new-method-ensures-complex-programs-are-bug-free-without-testing","status":"publish","type":"post","link":"https:\/\/michigan.it.umich.edu\/news\/2020\/06\/29\/new-method-ensures-complex-programs-are-bug-free-without-testing\/","title":{"rendered":"New method ensures complex programs are bug-free without testing"},"content":{"rendered":"\n<div class=\"wp-block-image\"><figure class=\"aligncenter size-large\"><img decoding=\"async\" src=\"https:\/\/cm-web-news-files.s3.amazonaws.com\/uploads\/2020\/06\/armada-content.jpg\" alt=\"(Five spools of yarn \u2014 two pink, one purple, two blue \u2014 each with a string of yarn extended out, tied to the others.)\"\/><figcaption>Multithreading is one common form of concurrent execution, allowing different instructions in a program to be processed simultaneously by one or more CPU cores. (Courtesy U-M\u2019s College of Computer Science and Engineering.)<\/figcaption><\/figure><\/div>\n\n\n\n<p class=\"wp-block-paragraph\"><a href=\"https:\/\/news.engin.umich.edu\/2020\/06\/new-method-ensures-complex-programs-are-bug-free-without-testing\/\">A team of researchers from the University of Michigan, Microsoft Research, and Carnegie Mellon have created Armada, a system that uses a technique called formal verification to prove whether a piece of software will output what it is designed to produce without bugs.<\/a>&nbsp;<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Armada targets software that uses concurrent execution, a method of performance boosting, and passes systems through a series of transformations until they break down into simpler representations. The developer only has to prove that each simplified step accurately represents the more complex program from the previous step by using Armada\u2019s high-level syntax to describe the simpler program and indicate a proof method that\u2019s needed to support the transformation. <\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The automatically-generated proof runs through a prover for verification. If it fails, the user changes their description or proof method to make a new one.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>A team of researchers from the University of Michigan, Microsoft Research, and Carnegie Mellon have created Armada, a system that uses a technique called formal verification to prove whether a piece of software will output what it is designed to produce without bugs.&nbsp; Armada targets software that uses concurrent execution, a method of performance boosting, and passes systems\u2026 <span class=\"read-more\"><a href=\"https:\/\/michigan.it.umich.edu\/news\/2020\/06\/29\/new-method-ensures-complex-programs-are-bug-free-without-testing\/\">Read More &raquo;<\/a><\/span><\/p>\n","protected":false},"author":1,"featured_media":19587,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_uag_custom_page_level_css":"","_umich_oidc_access":"","_monsterinsights_skip_tracking":false,"_monsterinsights_sitenote_active":false,"_monsterinsights_sitenote_note":"","_monsterinsights_sitenote_category":0,"_ef_editorial_meta_date_first-draft-date":"","_ef_editorial_meta_paragraph_assignment":"","_ef_editorial_meta_checkbox_needs-photo":"","_ef_editorial_meta_number_word-count":"","footnotes":""},"categories":[5],"tags":[852],"class_list":["post-19572","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-campus-news","tag-engineering"],"uagb_featured_image_src":{"full":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content.jpg",1560,1038,false],"thumbnail":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-200x133.jpg",200,133,true],"medium":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-300x200.jpg",300,200,true],"medium_large":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-768x511.jpg",665,442,true],"large":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-700x466.jpg",600,399,true],"1536x1536":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-1536x1022.jpg",1536,1022,true],"2048x2048":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content.jpg",1560,1038,false],"excerpt-thumbnail":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-200x140.jpg",200,140,true],"themonic-thumbnail":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-60x42.jpg",60,42,true],"ioslider-thumbnail":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-658x300.jpg",658,300,true],"post-thumbnail":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content-665x442.jpg",665,442,true],"400x250-crop":["https:\/\/michigan.it.umich.edu\/news\/wp-content\/uploads\/2020\/06\/armada-content.jpg",376,250,false]},"uagb_author_info":{"display_name":"News Staff","author_link":"https:\/\/michigan.it.umich.edu\/news\/author\/mitnewsadm\/"},"uagb_comment_info":0,"uagb_excerpt":"A team of researchers from the University of Michigan, Microsoft Research, and Carnegie Mellon have created Armada, a system that uses a technique called formal verification to prove whether a piece of software will output what it is designed to produce without bugs.&nbsp; Armada targets software that uses concurrent execution, a method of performance boosting,&hellip;","_links":{"self":[{"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/posts\/19572","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/comments?post=19572"}],"version-history":[{"count":2,"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/posts\/19572\/revisions"}],"predecessor-version":[{"id":19588,"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/posts\/19572\/revisions\/19588"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/media\/19587"}],"wp:attachment":[{"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/media?parent=19572"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/categories?post=19572"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/michigan.it.umich.edu\/news\/wp-json\/wp\/v2\/tags?post=19572"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}