{"id":181848,"date":"2024-02-01T14:25:49","date_gmt":"2024-02-01T20:25:49","guid":{"rendered":"https:\/\/lifeboat.com\/blog\/2024\/02\/ai-powered-proof-generator-helps-debug-software"},"modified":"2024-02-01T14:25:49","modified_gmt":"2024-02-01T20:25:49","slug":"ai-powered-proof-generator-helps-debug-software","status":"publish","type":"post","link":"https:\/\/lifeboat.com\/blog\/2024\/02\/ai-powered-proof-generator-helps-debug-software","title":{"rendered":"AI-Powered Proof Generator Helps Debug Software"},"content":{"rendered":"<p><a class=\"aligncenter blog-photo\" href=\"https:\/\/lifeboat.com\/blog.images\/ai-powered-proof-generator-helps-debug-software2.jpg\"><\/a><\/p>\n<p>Not all <a href=\"https:\/\/spectrum.ieee.org\/tag\/Software\" target=\"_self\" class=\"\">software<\/a> is perfect\u2014many apps, programs, and websites are released despite bugs. But the software behind critical systems like <a href=\"https:\/\/spectrum.ieee.org\/tag\/encryption\" target=\"_self\" class=\"\">cryptographic protocols<\/a>, <a href=\"https:\/\/spectrum.ieee.org\/topic\/biomedical\/\" target=\"_self\" class=\"\">medical devices<\/a>, and <a href=\"https:\/\/spectrum.ieee.org\/topic\/aerospace\/\" target=\"_self\" class=\"\">space shuttles<\/a> must be error-free, and ensuring the <a href=\"https:\/\/spectrum.ieee.org\/tla\" target=\"_self\" class=\"\">absence of bugs<\/a> requires going beyond code reviews and testing. It requires formal verification.<\/p>\n<p><a href=\"https:\/\/www.sciencedirect.com\/topics\/computer-science\/formal-verification\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">Formal verification<\/a> involves writing a mathematical proof of your code and is \u201cone of the hardest but also most powerful ways of making sure your code is correct,\u201d says <a href=\"https:\/\/people.cs.umass.edu\/~brun\/\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">Yuriy Brun<\/a>, a professor<strong><\/strong>at the <a href=\"https:\/\/www.umass.edu\/\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">University of Massachusetts Amherst<\/a>.<\/p>\n<p>To make formal verification easier, Brun and his colleagues devised a new AI-powered method called Baldur to automatically generate proofs. The accompanying <a href=\"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3616243\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">paper<\/a>, presented in December 2023 at the <a href=\"https:\/\/2023.esec-fse.org\/\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering<\/a> in San Francisco, won a <a href=\"https:\/\/2023.esec-fse.org\/info\/awards\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">Distinguished Paper award<\/a>. The team includes <a href=\"https:\/\/people.cs.umass.edu\/~efirst\/\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">Emily First<\/a>, who completed the study as part of her doctoral dissertation at UMass Amherst; Markus Rabe, a former researcher at <a href=\"https:\/\/spectrum.ieee.org\/tag\/Google\" target=\"_self\" class=\"\">Google<\/a>, where the study was conducted; and <a href=\"https:\/\/dependenttyp.es\/\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">Talia Ringer<\/a>, an assistant professor at the <a href=\"https:\/\/illinois.edu\/\" rel=\"noopener noreferrer\" target=\"_blank\" class=\"\">University of Illinois Urbana-Champaign<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Not all software is perfect\u2014many apps, programs, and websites are released despite bugs. But the software behind critical systems like cryptographic protocols, medical devices, and space shuttles must be error-free, and ensuring the absence of bugs requires going beyond code reviews and testing. It requires formal verification. Formal verification involves writing a mathematical proof of [\u2026]<\/p>\n","protected":false},"author":513,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[11,34,38,2229],"tags":[],"class_list":["post-181848","post","type-post","status-publish","format-standard","hentry","category-biotech-medical","category-cybercrime-malcode","category-engineering","category-mathematics"],"_links":{"self":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/posts\/181848","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/users\/513"}],"replies":[{"embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/comments?post=181848"}],"version-history":[{"count":0,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/posts\/181848\/revisions"}],"wp:attachment":[{"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/media?parent=181848"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/categories?post=181848"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/lifeboat.com\/blog\/wp-json\/wp\/v2\/tags?post=181848"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}