[{"command":"insert","method":null,"selector":".course-modal-ajax-placeholder-956179","data":"\u003Cdiv class=\u0022container content-rte\u0022\u003E\n  \u003Cdiv class=\u0022row\u0022\u003E\n    \u003Cdiv class=\u0022box col-md-6 bg-primary text-white\u0022\u003E\n      \u003Ch2 class=\u0022h1 text-left\u0022\u003E  Approches formelles pour la v\u00e9rification de programmes\n\u003C\/h2\u003E\n                  \u003Cdiv class=\u0022field-spacing\u0022\u003E\n        \u003Cdiv class=\u0022field__label h3 dash\u0022\u003EECTS :\n          2.5\n        \u003C\/div\u003E\n      \u003C\/div\u003E\n                  \u003Cdiv class=\u0022field-spacing\u0022\u003E\n        \u003Cdiv class=\u0022field__label h3 dash\u0022\u003ESemester:\n          Semestre 1\n        \u003C\/div\u003E\n      \u003C\/div\u003E\n            \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003ED\u00e9tail du volume horaire\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                          \u003Cspan class=\u0022field__label h4 mt-5 \u0022\u003ELecture:\u003C\/span\u003E\n                                      \u003Cspan\u003E18\u003C\/span\u003E\n                      \u003C\/div\u003E\n                                                                                        \u003C\/div\u003E\n        \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003ELangue d\u0026#039;enseignement\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                                      \u003Cspan\u003EFran\u00e7ais\u003C\/span\u003E\n                      \u003C\/div\u003E\n                  \u003C\/div\u003E\n        \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003EEnseignement \u00e0 distance\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                                      \u003Cspan\u003Enon\u003C\/span\u003E\n                      \u003C\/div\u003E\n                  \u003C\/div\u003E\n      \u003C\/div\u003E\n    \u003Cdiv class=\u0022box col-md-6\u0022\u003E\n            \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003EPr\u00e9requis\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                                      \u003Cspan\u003E\u003Cp\u003ECours de logique de base : logique propositionnelle, logique du premier ordre, s\u00e9mantique.\u003Cbr\u003E\n- Pratique d\u0027un langage de programmation.\u003Cbr\u003E\n- Cours de Th\u00e9orie des Langages : automates, grammaires hors-contextes.\u003C\/p\u003E\u003C\/span\u003E\n                      \u003C\/div\u003E\n                  \u003C\/div\u003E\n        \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003EProgramme \/ plan \/ contenus\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                                      \u003Cspan\u003E\u003Cp\u003ELes m\u00e9thodes formelles permettent de garantir la s\u00fbret\u00e9 d\u0027un syst\u00e8me par rapport \u00e0 une sp\u00e9cification donn\u00e9e. Dans ce cours, on \u00e9tudiera principalement les approches bas\u00e9es sur la preuve, qui requi\u00e8rent des\u003Cbr\u003E\nsp\u00e9cifications tr\u00e8s expressives. Apr\u00e8s un rappel sur la logique du\u003Cbr\u003E\npremier ordre, seront pr\u00e9sent\u00e9es les principales m\u00e9thodes pour faire des preuves assist\u00e9es par ordinateur : d\u0027une part des outils\u003Cbr\u003E\ncompl\u00e8tement automatiques comme les solveurs Satisfiabilit\u00e9 Modulo Th\u00e9orie et les prouveurs automatiques pour la logique du premier ordre ; d\u0027autre part les assistants \u00e0 la d\u00e9monstration qui sont plus puissants mais n\u00e9cessitent l\u0027intervention de l\u0027utilisateur.\u003C\/p\u003E\n\u003Cp\u003EIl sera \u00e9galement \u00e9tudi\u00e9 comment ajouter des sp\u00e9cifications \u00e0 un\u003Cbr\u003E\nprogramme, sous la forme d\u0027annotations et\/ou de contrats. Pour v\u00e9rifier ces annotations, par le biais de la logique de Hoare, les annotations sont transform\u00e9es en obligations de preuve dont la d\u00e9monstration\u003Cbr\u003E\ngarantit le respect de la sp\u00e9cification avant m\u00eame toute ex\u00e9cution. Le cours comporte \u00e9galement une initiation \u00e0 la manipulation du plugin WP\u003Cbr\u003E\nde la plateforme d\u0027analyse des programmes C appel\u00e9e Frama-C.\u003C\/p\u003E\n\u003Cp\u003ELa derni\u00e8re partie du cours vise \u00e0 pr\u00e9senter les techniques\u003Cbr\u003E\nd\u0027apprentissage permettant de construire automatiquement des mod\u00e8les de syst\u00e8mes, sous la forme de machines \u00e0 \u00e9tats, en interagissant avec eux. Ces mod\u00e8les peuvent ensuite servir de sujet pour d\u00e9montrer\u003Cbr\u003E\ndes propri\u00e9t\u00e9s de s\u00fbret\u00e9 ou de s\u00e9curit\u00e9. Ils ont notamment \u00e9t\u00e9\u003Cbr\u003E\nexploit\u00e9s pour d\u00e9tecter des trous de s\u00e9curit\u00e9 dans des sites web,\u003Cbr\u003E\nou pour reconstruire les sp\u00e9cifications de syst\u00e8mes en r\u00e9ing\u00e9nierie logicielle. Le cours pr\u00e9sente les grandes familles d\u0027algorithmes, actifs ou passifs, utilis\u00e9s en inf\u00e9rence grammaticale exacte.\u003C\/p\u003E\u003C\/span\u003E\n                      \u003C\/div\u003E\n                  \u003C\/div\u003E\n                \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003EOrganisation g\u00e9n\u00e9rale et modalit\u00e9s p\u00e9dagogiques\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                                      \u003Cspan\u003E\u003Cp\u003ELe cours se d\u00e9compose en trois parties :\u003Cbr\u003E\n1. Introduction \u00e0 la n\u00e9cessit\u00e9 des approches formelle. Rappel logique du premier ordre. Sp\u00e9cification de programmes imp\u00e9ratifs. Preuve de programme : Logique de Hoare. Calcul de plus faible pr\u00e9condition.\u003Cbr\u003E\nPreuve de programme sur machine \u00e0 l\u0027aide du plugin WP de Frama-C.\u003C\/p\u003E\n\u003Cp\u003E2. Preuve m\u00e9canis\u00e9e. Preuve automatique : SAT, SMT et r\u00e9solution.\u003Cbr\u003E\n\u0026nbsp;\u0026nbsp;D\u00e9duction naturelle. Assistant \u00e0 la d\u00e9monstration. Illustration avec Rocq. Utilisation sur machine des outils de preuve m\u00e9canis\u00e9e.\u003C\/p\u003E\n\u003Cp\u003E3. Apprentissage de mod\u00e8les de syst\u00e8mes : inf\u00e9rence grammaticale, apprentissage par requ\u00eate, apprentissage passif d\u0027automates et de grammaires.\u003C\/p\u003E\u003C\/span\u003E\n                      \u003C\/div\u003E\n                  \u003C\/div\u003E\n                        \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003EBibliographie\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                                      \u003Cspan\u003E\u003Cp\u003ELogic and proof, cours de Lawrence Paulson :\u003Cbr\u003E\n\u0026nbsp;\u003Ca rel=\u0022nofollow noopener noreferrer\u0022 target=\u0022_blank\u0022 href=\u0022https:\/\/www.cl.cam.ac.uk\/teaching\/1920\/LogicProof\/logic-notes.pdf\u0022\u003Ehttps:\/\/www.cl.cam.ac.uk\/teaching\/1920\/LogicProof\/logic-notes.pdf\u003C\/a\u003E\u003Cbr\u003E\n- Travaux fondateurs de Dana Angluin : \u00ab Learning Regular Sets from Queries and Counter-Examples \u00bb, Information and Control, vol. 75, no 2,\u200e 1987, p. 87\u2013106\u003Cbr\u003E\n- Livre de Colin de la Higuera : \u0022Grammatical Inference: Learning\u003Cbr\u003E\n\u0026nbsp;Automata and Grammars\u0022, Cambridge University Press, 2010\u003C\/p\u003E\u003C\/span\u003E\n                      \u003C\/div\u003E\n                  \u003C\/div\u003E\n        \u003Cdiv class=\u0022field-spacing\u0022\u003E\n      \u003Cdiv class=\u0022field__label h3 dash\u0022\u003ENature de l\u0026#039;\u00e9valuation\u003C\/div\u003E\n                        \u003Cdiv class=\u0022mt-5 text-justify\u0022\u003E\n                                      \u003Cspan\u003EEvaluation Terminale\u003C\/span\u003E\n                      \u003C\/div\u003E\n                  \u003C\/div\u003E\n      \u003C\/div\u003E\n  \u003C\/div\u003E\n\u003C\/div\u003E\n","settings":null}]