{"id":1216,"date":"2025-07-11T18:32:24","date_gmt":"2025-07-11T16:32:24","guid":{"rendered":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/?p=1216"},"modified":"2025-07-11T18:32:24","modified_gmt":"2025-07-11T16:32:24","slug":"july-2025-talk-by-andre-maroneze","status":"publish","type":"post","link":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2025\/07\/11\/july-2025-talk-by-andre-maroneze\/","title":{"rendered":"[July 2025] Talk by Andr\u00e9 Maroneze"},"content":{"rendered":"\n<p><strong>Frama-C\/Eva: a concrete application of abstract interpretation<\/strong><br>Andr\u00e9 Maroneze (CEA LIST)<br><em>July 16, 2025<\/em><br>The C language is widely used for critical systems, despite its memory unsafety. The Frama-C platform provides static and dynamic code analyses, based on formal verification techniques, to provide guarantees for C code bases. Between testing and full program proof, the Eva analyzer allows automatic identification of several kinds of undefined behaviors. It can be seen as an \u201cabstract debugger\u201d, and help understand what the code does. With some experience, it can scale up to 100k\u2019s lines of code. This presentation will focus on practical examples, some theoretical foundations, and ongoing challenges concerning the application of abstract interpretation to C code analysis.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Frama-C\/Eva: a concrete application of abstract interpretationAndr\u00e9 Maroneze (CEA LIST)July 16, 2025The C language is widely used for critical systems, despite its memory unsafety. The Frama-C platform provides static and dynamic code analyses, based on formal verification techniques, to provide guarantees for C code bases. Between testing and full program proof, the Eva analyzer allows &hellip; <a href=\"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2025\/07\/11\/july-2025-talk-by-andre-maroneze\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;[July 2025] Talk by Andr\u00e9 Maroneze&#8221;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-1216","post","type-post","status-publish","format-standard","hentry","category-non-classe"],"_links":{"self":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/1216","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/comments?post=1216"}],"version-history":[{"count":1,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/1216\/revisions"}],"predecessor-version":[{"id":1218,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/1216\/revisions\/1218"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=1216"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/categories?post=1216"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/tags?post=1216"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}