{"id":377,"date":"2023-02-05T16:31:25","date_gmt":"2023-02-05T15:31:25","guid":{"rendered":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/?p=377"},"modified":"2023-02-05T16:31:25","modified_gmt":"2023-02-05T15:31:25","slug":"fev-2023-keynote-of-julien-signoles-cea-list","status":"publish","type":"post","link":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2023\/02\/05\/fev-2023-keynote-of-julien-signoles-cea-list\/","title":{"rendered":"[Fev. 2023] Keynote of Julien Signoles, CEA List"},"content":{"rendered":"\n<p><a><strong>Frama-C, une plateforme open-source d&#8217;analyses de programmes C<\/strong><\/a><\/p>\n\n\n\n<p><em>SR1, Monday, February 13, 2023, 13h30<\/em><\/p>\n\n\n\n<p>Cet expos\u00e9 pr\u00e9sentera Frama-C, une plateforme open-source d\u00e9di\u00e9e \u00e0 l&#8217;analyse de programmes \u00e9crits en langage C. Apr\u00e8s un aper\u00e7u g\u00e9n\u00e9ral de la plateforme, nous introduirons ses principaux greffons d&#8217;analyse. Ainsi, nous expliquerons d&#8217;abord comment prouver l&#8217;absence de comportements ind\u00e9finis (ou les d\u00e9tecter s&#8217;il y en a) \u00e0 l&#8217;aide d&#8217;Eva, le greffon d&#8217;analyse de valeurs par interpr\u00e9tation abstraite, nous introduirons ensuite comment prouver des propri\u00e9t\u00e9s fonctionnelles \u00e0 l&#8217;aide du greffon WP d\u00e9di\u00e9 \u00e0 la v\u00e9rification d\u00e9ductive, puis nous pr\u00e9senterons comment d\u00e9tecter des erreurs avanc\u00e9es en cours d&#8217;ex\u00e9cution d&#8217;un programme, \u00e0 l&#8217;aide d&#8217;E-ACSL, le greffon d\u00e9di\u00e9 \u00e0 la v\u00e9rification \u00e0 l&#8217;ex\u00e9cution. Enfin, nous montrerons quelques usages plus avanc\u00e9s combinant diff\u00e9rentes analyses. Les diff\u00e9rentes techniques pr\u00e9sent\u00e9es seront illustr\u00e9es \u00e0 travers diff\u00e9rents exemples r\u00e9els provenant de domaines applicatifs vari\u00e9s (nucl\u00e9aire, avionique, carte \u00e0 puce, &#8230;).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Frama-C, une plateforme open-source d&#8217;analyses de programmes C SR1, Monday, February 13, 2023, 13h30 Cet expos\u00e9 pr\u00e9sentera Frama-C, une plateforme open-source d\u00e9di\u00e9e \u00e0 l&#8217;analyse de programmes \u00e9crits en langage C. Apr\u00e8s un aper\u00e7u g\u00e9n\u00e9ral de la plateforme, nous introduirons ses principaux greffons d&#8217;analyse. Ainsi, nous expliquerons d&#8217;abord comment prouver l&#8217;absence de comportements ind\u00e9finis (ou les &hellip; <a href=\"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2023\/02\/05\/fev-2023-keynote-of-julien-signoles-cea-list\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;[Fev. 2023] Keynote of Julien Signoles, CEA List&#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-377","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\/377","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=377"}],"version-history":[{"count":1,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/377\/revisions"}],"predecessor-version":[{"id":379,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/377\/revisions\/379"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=377"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/categories?post=377"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/tags?post=377"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}