{"id":348,"date":"2022-11-30T18:54:35","date_gmt":"2022-11-30T17:54:35","guid":{"rendered":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/?p=348"},"modified":"2022-11-30T18:59:07","modified_gmt":"2022-11-30T17:59:07","slug":"the-three-year-comemov-project-is-funded-by-anr","status":"publish","type":"post","link":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2022\/11\/30\/the-three-year-comemov-project-is-funded-by-anr\/","title":{"rendered":"[Nov. 2022] The three-year CoMeMoV project is funded by ANR"},"content":{"rendered":"\n<p><a href=\"https:\/\/frama-c.com\">Frama-C<\/a>, a framework for the analysis and verification of C programs, with its WP plugin, provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial strength programs, this combination already makes WP mature enough to be deployed for proving industrial critical embedded software. However, several theoretical and practical issues still persist. The goal of <a href=\"http:\/\/comemov.github.io\">CoMeMoV<\/a> is to tackle these issues to scale on deductive verification of complex programs. CoMeMoV, lead by Fr\u00e9d\u00e9ric Loulergue, is a joint project of Universit\u00e9 d&#8217;Orl\u00e9ans (LIFO, LMV Team), CEA List and Thales Research &amp; Technology.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Frama-C, a framework for the analysis and verification of C programs, with its WP plugin, provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial strength programs, this combination already makes WP mature enough to be deployed for proving industrial critical &hellip; <a href=\"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2022\/11\/30\/the-three-year-comemov-project-is-funded-by-anr\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;[Nov. 2022] The three-year CoMeMoV project is funded by ANR&#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-348","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\/348","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=348"}],"version-history":[{"count":2,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/348\/revisions"}],"predecessor-version":[{"id":357,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/348\/revisions\/357"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=348"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/categories?post=348"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/tags?post=348"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}