{"id":2261,"date":"2021-11-05T14:45:14","date_gmt":"2021-11-05T13:45:14","guid":{"rendered":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/?p=2261"},"modified":"2021-11-05T17:43:58","modified_gmt":"2021-11-05T16:43:58","slug":"ahmed-bouajjani-des-automates-pour-verifier-les-programmes","status":"publish","type":"post","link":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/ahmed-bouajjani-des-automates-pour-verifier-les-programmes\/","title":{"rendered":"Ahmed Bouajjani : des automates pour v\u00e9rifier les programmes"},"content":{"rendered":"

[et_pb_section bb_built=\u00a0\u00bb1″ next_background_color=\u00a0\u00bb#000000″ inner_width=\u00a0\u00bbauto\u00a0\u00bb inner_max_width=\u00a0\u00bbnone\u00a0\u00bb][et_pb_row][et_pb_column type=\u00a0\u00bb3_4″][et_pb_text admin_label=\u00a0\u00bbIntro\u00a0\u00bb _builder_version=\u00a0\u00bb3.22.1″ module_id=\u00a0\u00bbintro\u00a0\u00bb text_text_shadow_horizontal_length=\u00a0\u00bbtext_text_shadow_style,%91object Object%93″ text_text_shadow_vertical_length=\u00a0\u00bbtext_text_shadow_style,%91object Object%93″ text_text_shadow_blur_strength=\u00a0\u00bbtext_text_shadow_style,%91object Object%93″ link_text_shadow_horizontal_length=\u00a0\u00bblink_text_shadow_style,%91object Object%93″ link_text_shadow_vertical_length=\u00a0\u00bblink_text_shadow_style,%91object Object%93″ link_text_shadow_blur_strength=\u00a0\u00bblink_text_shadow_style,%91object Object%93″ ul_text_shadow_horizontal_length=\u00a0\u00bbul_text_shadow_style,%91object Object%93″ ul_text_shadow_vertical_length=\u00a0\u00bbul_text_shadow_style,%91object Object%93″ ul_text_shadow_blur_strength=\u00a0\u00bbul_text_shadow_style,%91object Object%93″ ol_text_shadow_horizontal_length=\u00a0\u00bbol_text_shadow_style,%91object Object%93″ ol_text_shadow_vertical_length=\u00a0\u00bbol_text_shadow_style,%91object Object%93″ ol_text_shadow_blur_strength=\u00a0\u00bbol_text_shadow_style,%91object Object%93″ quote_text_shadow_horizontal_length=\u00a0\u00bbquote_text_shadow_style,%91object Object%93″ quote_text_shadow_vertical_length=\u00a0\u00bbquote_text_shadow_style,%91object Object%93″ quote_text_shadow_blur_strength=\u00a0\u00bbquote_text_shadow_style,%91object Object%93″ header_text_shadow_horizontal_length=\u00a0\u00bbheader_text_shadow_style,%91object Object%93″ header_text_shadow_vertical_length=\u00a0\u00bbheader_text_shadow_style,%91object Object%93″ header_text_shadow_blur_strength=\u00a0\u00bbheader_text_shadow_style,%91object Object%93″ header_2_text_shadow_horizontal_length=\u00a0\u00bbheader_2_text_shadow_style,%91object Object%93″ header_2_text_shadow_vertical_length=\u00a0\u00bbheader_2_text_shadow_style,%91object Object%93″ header_2_text_shadow_blur_strength=\u00a0\u00bbheader_2_text_shadow_style,%91object Object%93″ header_3_text_shadow_horizontal_length=\u00a0\u00bbheader_3_text_shadow_style,%91object Object%93″ header_3_text_shadow_vertical_length=\u00a0\u00bbheader_3_text_shadow_style,%91object Object%93″ header_3_text_shadow_blur_strength=\u00a0\u00bbheader_3_text_shadow_style,%91object Object%93″ header_4_text_shadow_horizontal_length=\u00a0\u00bbheader_4_text_shadow_style,%91object Object%93″ header_4_text_shadow_vertical_length=\u00a0\u00bbheader_4_text_shadow_style,%91object Object%93″ header_4_text_shadow_blur_strength=\u00a0\u00bbheader_4_text_shadow_style,%91object Object%93″ header_5_text_shadow_horizontal_length=\u00a0\u00bbheader_5_text_shadow_style,%91object Object%93″ header_5_text_shadow_vertical_length=\u00a0\u00bbheader_5_text_shadow_style,%91object Object%93″ header_5_text_shadow_blur_strength=\u00a0\u00bbheader_5_text_shadow_style,%91object Object%93″ header_6_text_shadow_horizontal_length=\u00a0\u00bbheader_6_text_shadow_style,%91object Object%93″ header_6_text_shadow_vertical_length=\u00a0\u00bbheader_6_text_shadow_style,%91object Object%93″ header_6_text_shadow_blur_strength=\u00a0\u00bbheader_6_text_shadow_style,%91object Object%93″ z_index_tablet=\u00a0\u00bb500″]<\/p>\n

\n
\n
\n

Un article co-r\u00e9dig\u00e9 par Ahmed Bouajjani, co-responsable de la sp\u00e9cialit\u00e9 Syst\u00e8mes Informatiques Embarqu\u00e9s de l’\u00e9cole, a \u00e9t\u00e9 prim\u00e9 lors de la conf\u00e9rence CONCUR.\u00a0<\/p>\n<\/div>\n<\/div>\n<\/div>\n

[\/et_pb_text][\/et_pb_column][et_pb_column type=\u00a0\u00bb1_4″][\/et_pb_column][\/et_pb_row][et_pb_row][et_pb_column type=\u00a0\u00bb3_4″][et_pb_text _builder_version=\u00a0\u00bb3.22.1″ module_id=\u00a0\u00bbcontenu\u00a0\u00bb text_text_shadow_horizontal_length=\u00a0\u00bbtext_text_shadow_style,%91object Object%93″ text_text_shadow_vertical_length=\u00a0\u00bbtext_text_shadow_style,%91object Object%93″ text_text_shadow_blur_strength=\u00a0\u00bbtext_text_shadow_style,%91object Object%93″ link_text_shadow_horizontal_length=\u00a0\u00bblink_text_shadow_style,%91object Object%93″ link_text_shadow_vertical_length=\u00a0\u00bblink_text_shadow_style,%91object Object%93″ link_text_shadow_blur_strength=\u00a0\u00bblink_text_shadow_style,%91object Object%93″ ul_text_shadow_horizontal_length=\u00a0\u00bbul_text_shadow_style,%91object Object%93″ ul_text_shadow_vertical_length=\u00a0\u00bbul_text_shadow_style,%91object Object%93″ ul_text_shadow_blur_strength=\u00a0\u00bbul_text_shadow_style,%91object Object%93″ ol_text_shadow_horizontal_length=\u00a0\u00bbol_text_shadow_style,%91object Object%93″ ol_text_shadow_vertical_length=\u00a0\u00bbol_text_shadow_style,%91object Object%93″ ol_text_shadow_blur_strength=\u00a0\u00bbol_text_shadow_style,%91object Object%93″ quote_text_shadow_horizontal_length=\u00a0\u00bbquote_text_shadow_style,%91object Object%93″ quote_text_shadow_vertical_length=\u00a0\u00bbquote_text_shadow_style,%91object Object%93″ quote_text_shadow_blur_strength=\u00a0\u00bbquote_text_shadow_style,%91object Object%93″ header_text_shadow_horizontal_length=\u00a0\u00bbheader_text_shadow_style,%91object Object%93″ header_text_shadow_vertical_length=\u00a0\u00bbheader_text_shadow_style,%91object Object%93″ header_text_shadow_blur_strength=\u00a0\u00bbheader_text_shadow_style,%91object Object%93″ header_2_text_shadow_horizontal_length=\u00a0\u00bbheader_2_text_shadow_style,%91object Object%93″ header_2_text_shadow_vertical_length=\u00a0\u00bbheader_2_text_shadow_style,%91object Object%93″ header_2_text_shadow_blur_strength=\u00a0\u00bbheader_2_text_shadow_style,%91object Object%93″ header_3_text_shadow_horizontal_length=\u00a0\u00bbheader_3_text_shadow_style,%91object Object%93″ header_3_text_shadow_vertical_length=\u00a0\u00bbheader_3_text_shadow_style,%91object Object%93″ header_3_text_shadow_blur_strength=\u00a0\u00bbheader_3_text_shadow_style,%91object Object%93″ header_4_text_shadow_horizontal_length=\u00a0\u00bbheader_4_text_shadow_style,%91object Object%93″ header_4_text_shadow_vertical_length=\u00a0\u00bbheader_4_text_shadow_style,%91object Object%93″ header_4_text_shadow_blur_strength=\u00a0\u00bbheader_4_text_shadow_style,%91object Object%93″ header_5_text_shadow_horizontal_length=\u00a0\u00bbheader_5_text_shadow_style,%91object Object%93″ header_5_text_shadow_vertical_length=\u00a0\u00bbheader_5_text_shadow_style,%91object Object%93″ header_5_text_shadow_blur_strength=\u00a0\u00bbheader_5_text_shadow_style,%91object Object%93″ header_6_text_shadow_horizontal_length=\u00a0\u00bbheader_6_text_shadow_style,%91object Object%93″ header_6_text_shadow_vertical_length=\u00a0\u00bbheader_6_text_shadow_style,%91object Object%93″ header_6_text_shadow_blur_strength=\u00a0\u00bbheader_6_text_shadow_style,%91object Object%93″ z_index_tablet=\u00a0\u00bb500″ text_orientation=\u00a0\u00bbjustified\u00a0\u00bb]<\/p>\n

Lire l’article sur le site du CNRS<\/a><\/p>\n

 <\/p>\n

Pr\u00e8s de 25 ans apr\u00e8s sa publication, un article co-r\u00e9dig\u00e9 par\u00a0Ahmed Bouajjani<\/a>\u00a0de l\u2019Institut de Recherche en Informatique Fondamentale<\/a>\u00a0(IRIF – CNRS\/Universit\u00e9 Paris Cit\u00e9) a \u00e9t\u00e9 prim\u00e9 \u00e0 la conf\u00e9rence CONCUR pour son influence sur la v\u00e9rification de mod\u00e8les. Ces travaux proposent des algorithmes de v\u00e9rification de syst\u00e8mes dits \u00ab \u00e0 pile \u00bb. L\u2019approche utilise des automates pour repr\u00e9senter de mani\u00e8re finie et manipuler des ensembles infinis de configurations de syst\u00e8mes.<\/p>\n

\n
\n
\n
\n

Les syst\u00e8mes informatiques ont besoin d\u2019\u00eatre inspect\u00e9s de mani\u00e8re formelle et syst\u00e9matique pour savoir s\u2019ils vont fonctionner correctement. Ahmed\u00a0Bouajjani, professeur \u00e0 l\u2019Universit\u00e9 Paris Cit\u00e9 et responsable du p\u00f4le\u00a0Automates, structures et v\u00e9rification<\/u><\/span><\/a>\u00a0\u00e0 l\u2019IRIF, explore des probl\u00e8mes de sp\u00e9cification, de mod\u00e9lisation et de v\u00e9rification formelle des syst\u00e8mes. Une grande partie de ses travaux est consacr\u00e9e aux m\u00e9thodes de v\u00e9rification s\u2019apparentant au\u00a0model checking<\/em>, ou v\u00e9rification de mod\u00e8les, pour diff\u00e9rentes classes de syst\u00e8mes infinis.<\/p>\n

\u00ab\u2009Ma recherche vise \u00e0 concevoir des m\u00e9thodes et des outils permettant aux programmeurs d\u2019am\u00e9liorer la qualit\u00e9 de leurs programmes, notamment en termes de fiabilit\u00e9<\/em>, explique Ahmed\u00a0Bouajjani.\u00a0Je travaille \u00e0 la v\u00e9rification automatique qu\u2019un programme satisfait bien les propri\u00e9t\u00e9s qu\u2019il doit satisfaire, puis \u00e0 la correction des \u00e9ventuels probl\u00e8mes<\/em>.\u2009\u00bb Parmi les diff\u00e9rentes approches, Ahmed\u00a0Bouajjani s\u2019est sp\u00e9cialis\u00e9 dans la v\u00e9rification algorithmique.<\/p>\n

Son article fondateur\u00a0Reachability analysis of pushdown automata: application to model-checking<\/u><\/span><\/a><\/em>, co-\u00e9crit avec\u00a0Javier Esparza<\/span><\/a>1<\/a>\u00a0et\u00a0Oded Maler<\/u><\/span><\/a>, a re\u00e7u le prix\u00a0Test-of-time<\/u><\/span><\/a><\/em>\u00a0de la conf\u00e9rence CONCUR2<\/a>\u00a02021 apr\u00e8s avoir \u00e9t\u00e9 pr\u00e9sent\u00e9 \u00e0 la conf\u00e9rence CONCUR\u2026 1997\u2009! Cette r\u00e9compense se laisse en effet un long recul pour observer le v\u00e9ritable impact des articles qu\u2019il distingue, avec cette ann\u00e9e quatre laur\u00e9ats pour des travaux publi\u00e9s entre 1994 et 1999. Ahmed\u00a0Bouajjani \u00e9tait dans les ann\u00e9es\u00a090 membre du laboratoire VERIMAG (CNRS\/Universit\u00e9 Grenoble Alpes), dirig\u00e9 \u00e0 l\u2019\u00e9poque par\u00a0Joseph\u00a0Sifakis<\/u><\/span><\/a>, actuellement directeur de recherche CNRS \u00e9m\u00e9rite, premier fran\u00e7ais \u00e0 obtenir le prix Turing pour ses travaux sur le\u00a0model checking<\/em>.<\/p>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n

\n
\n
\n
Ce travail \u00e9tait au d\u00e9part de nature th\u00e9orique, mais il a eu par la suite un impact important gr\u00e2ce \u00e0 la simplicit\u00e9, \u00e0 la puissance et aux nombreuses applications des syst\u00e8mes \u00e0 pile.<\/div>\n<\/blockquote>\n<\/div>\n<\/div>\n
\n
\n
\n
\n

\u00ab<\/em>\u2009\u00c0<\/em>\u00a0l\u2019\u00e9poque, les travaux sur le\u00a0<\/em>model-checking\u00a0consid\u00e9raient essentiellement des syst\u00e8mes avec un nombre fini de configurations possibles<\/em>, pr\u00e9cise Ahmed\u00a0Bouajjani.\u00a0Ces mod\u00e8les ne sont g\u00e9n\u00e9ralement pas assez expressifs pour repr\u00e9senter fid\u00e8lement les comportements des syst\u00e8mes logiciels, et nos travaux ont contribu\u00e9 au passage \u00e0 des mod\u00e8<\/em>les au nombre infini de configurations. Le mod\u00e8le des syst\u00e8mes \u00e0 pile offre assez d\u2019expressivit\u00e9 pour servir \u00e0 ces applications, tout en \u00e9tant assez restreint pour conserver de bonnes propri\u00e9t\u00e9s algorithmiques.\u2009\u00bb<\/em><\/p>\n

Le mod\u00e8le des syst\u00e8mes \u00e0 pile consiste en des machines abstraites poss\u00e9dant un nombre fini d\u2019\u00e9tats de contr\u00f4le, et o\u00f9 chaque changement d\u2019\u00e9tat permet de r\u00e9aliser une op\u00e9ration sur des donn\u00e9es structur\u00e9es en pile. Trois actions sont disponibles\u00a0: v\u00e9rifier si la pile est vide, ajouter quelque chose sur la pile ou enlever l\u2019\u00e9l\u00e9ment en sommet de pile. Dans ces syst\u00e8mes, la taille de la pile n\u2019est pas born\u00e9e et donc peut cro\u00eetre arbitrairement, rendant ainsi le nombre de configurations possibles d\u2019un syst\u00e8me \u00e0 pile infini.<\/p>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n

\n
\n
\n
L\u2019ensemble des configurations de pile peut \u00eatre vu comme un ensemble de s\u00e9quences, or un ensemble de s\u00e9quences est un langage, qui peut \u00eatre repr\u00e9sent\u00e9 par un automate.<\/div>\n<\/blockquote>\n
\u00a0<\/div>\n<\/div>\n<\/div>\n
\n
\n
\n
\n

Les automates offrent ainsi une repr\u00e9sentation compacte et finie d\u2019ensembles infinis de configurations de pile. Dans les travaux pr\u00e9sent\u00e9s \u00e0 CONCUR\u00a01997, des algorithmes de\u00a0model-checking<\/em>\u00a0sont d\u00e9finis pour v\u00e9rifier qu\u2019une certaine propri\u00e9t\u00e9 exprim\u00e9e dans un langage logique g\u00e9n\u00e9ral est bien satisfaite par un syst\u00e8me \u00e0 pile donn\u00e9. Plus g\u00e9n\u00e9ralement, gr\u00e2ce \u00e0 l\u2019approche utilisant les automates, ces algorithmes permettent de calculer l\u2019ensemble des configurations du syst\u00e8me qui satisfont la propri\u00e9t\u00e9 cibl\u00e9e.<\/p>\n

Depuis, Ahmed\u00a0Bouajjani a explor\u00e9 de multiples g\u00e9n\u00e9ralisations et applications des automates \u00e0 pile, ainsi que diff\u00e9rentes classes de syst\u00e8mes informatiques. Ses travaux r\u00e9cents portent sur la concurrence et sur les syst\u00e8mes distribu\u00e9s, o\u00f9 il faut assurer un certain niveau de consistance entre les donn\u00e9es stock\u00e9es et trait\u00e9es sur plusieurs machines distantes \u00e0 la fois.<\/p>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n

Lire l’article publi\u00e9 sur le site du CNRS<\/a><\/p>\n

Source: https:\/\/www.ins2i.cnrs.fr\/fr\/cnrsinfo\/ahmed-bouajjani-des-automates-pour-verifier-les-programmes<\/p>\n

[\/et_pb_text][\/et_pb_column][et_pb_column type=\u00a0\u00bb1_4″][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section bb_built=\u00a0\u00bb1″ specialty=\u00a0\u00bboff\u00a0\u00bb _builder_version=\u00a0\u00bb3.21″ custom_padding=\u00a0\u00bb0px||0px|\u00a0\u00bb prev_background_color=\u00a0\u00bb#000000″ inner_width=\u00a0\u00bbauto\u00a0\u00bb inner_max_width=\u00a0\u00bbnone\u00a0\u00bb][et_pb_row _builder_version=\u00a0\u00bb3.19.11″ width=\u00a0\u00bb80%\u00a0\u00bb max_width=\u00a0\u00bb1080px\u00a0\u00bb][et_pb_column type=\u00a0\u00bb4_4″][et_pb_text admin_label=\u00a0\u00bb\u00c0 lire aussi\u00a0\u00bb _builder_version=\u00a0\u00bb3.21″]<\/p>\n

\u00c0<\/span> lire aussi<\/h2>\n

[\/et_pb_text][et_pb_blog _builder_version=\u00a0\u00bb3.21″ posts_number=\u00a0\u00bb4″ include_categories=\u00a0\u00bb13″ show_author=\u00a0\u00bboff\u00a0\u00bb show_date=\u00a0\u00bboff\u00a0\u00bb show_pagination=\u00a0\u00bboff\u00a0\u00bb border_width_bottom_fullwidth=\u00a0\u00bb1px\u00a0\u00bb border_color_bottom_fullwidth=\u00a0\u00bbrgba(51,51,51,0.18)\u00a0\u00bb custom_padding=\u00a0\u00bb||50px|\u00a0\u00bb module_id=\u00a0\u00bbpage_type_blog\u00a0\u00bb header_level=\u00a0\u00bbh4″ \/][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"

<\/div>\n

Un article co-r\u00e9dig\u00e9 par Ahmed Bouajjani, co-responsable de la sp\u00e9cialit\u00e9 Syst\u00e8mes Informatiques Embarqu\u00e9s de l’\u00e9cole, a \u00e9t\u00e9 prim\u00e9 lors de la conf\u00e9rence CONCUR.\u00a0 <\/p>\n

<\/div>\n

Lire l’article sur le site du CNRS   Pr\u00e8s de 25 ans apr\u00e8s sa publication, un article co-r\u00e9dig\u00e9 par\u00a0Ahmed Bouajjani\u00a0de l\u2019Institut de Recherche en Informatique Fondamentale\u00a0(IRIF – CNRS\/Universit\u00e9 Paris Cit\u00e9)… Lire la suite Ahmed Bouajjani : des automates pour v\u00e9rifier les programmes<\/span><\/a><\/p>\n","protected":false},"author":254,"featured_media":2270,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"","_et_gb_content_width":"","footnotes":""},"categories":[1,29],"tags":[],"class_list":["post-2261","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-ecole-d-ingenieur-denis-diderot","category-eidd-dans-la-presse"],"_links":{"self":[{"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/posts\/2261","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/users\/254"}],"replies":[{"embeddable":true,"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/comments?post=2261"}],"version-history":[{"count":8,"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/posts\/2261\/revisions"}],"predecessor-version":[{"id":2272,"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/posts\/2261\/revisions\/2272"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/media\/2270"}],"wp:attachment":[{"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/media?parent=2261"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/categories?post=2261"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/wordpress-test.app.u-pariscite.fr\/eidd\/wp-json\/wp\/v2\/tags?post=2261"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}