{"id":12126,"date":"2023-06-08T11:42:49","date_gmt":"2023-06-08T10:42:49","guid":{"rendered":"https:\/\/cyberschool.univ-rennes.fr\/?page_id=12126"},"modified":"2026-03-12T14:29:51","modified_gmt":"2026-03-12T13:29:51","slug":"software-formal-analysis-and-design","status":"publish","type":"page","link":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/","title":{"rendered":"Software formal analysis and design"},"content":{"rendered":"\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Teaching goals<\/h2>\n                        <p>L\u2019UE ACF vise \u00e0 initier les \u00e9tudiants \u00e0 l\u2019utilisation de m\u00e9thodes formelles pour la sp\u00e9cification et le d\u00e9veloppement de logiciels s\u00fbrs. L\u2019accent est mis sur la compr\u00e9hension des formules logiques et sur leur utilisation pour la sp\u00e9cification de propri\u00e9t\u00e9s de programmes. Les programmes consid\u00e9r\u00e9s seront d\u00e9finis dans un style fonctionnel. L\u2019outil de d\u00e9veloppement formel utilis\u00e9 est Isabelle\/HOL et le langage d\u2019exportation et d\u2019int\u00e9gration choisi est Scala.<\/p>\n\n        <\/div>\n    <\/div>\n<\/section>\n\n\n\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Course description<\/h2>\n                        <section class=\"txt\">\n<div class=\"container\">\n<div class=\"bloc-txt\">\n<p>L\u2019UE ACF vise \u00e0 initier les \u00e9tudiants \u00e0 l\u2019utilisation de m\u00e9thodes formelles pour la sp\u00e9cification et le d\u00e9veloppement de logiciels s\u00fbrs.<\/p>\n<\/div>\n<\/div>\n<\/section>\n\n        <\/div>\n    <\/div>\n<\/section>\n\n\n\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Course content<\/h2>\n                        <ul>\n<li>Cours\n<ul>\n<li>Logique propositionnelle, logique du premier ordre et mod\u00e8les.<\/li>\n<li>Termes, fonctions, lambda-calcul et types<\/li>\n<li>Fonctions r\u00e9cursives<\/li>\n<li>Principes et tactiques de preuve<\/li>\n<li>Programmation certifi\u00e9e<\/li>\n<li>Techniques de v\u00e9rification de programmes<\/li>\n<\/ul>\n<\/li>\n<li>Travaux pratiques\n<ul>\n<li>Mise en situation\u00a0: tentative de programmation correcte d\u2019un algorithme non trivial<\/li>\n<li>Initiation \u00e0 la programmation et \u00e0 la preuve dans un assistant de preuve (Isabelle\/HOL)<\/li>\n<li>Initiation \u00e0 la programmation Scala<\/li>\n<li>Projet 1 : programmation et v\u00e9rification d&#8217;un outil de comparaison de<br \/>\npolitique de s\u00e9curit\u00e9 pour un firewall simplifi\u00e9<\/li>\n<li>Projet 2 : programmation et v\u00e9rification d\u2019un analyseur statique<\/li>\n<li>Projet 3 : programmation et v\u00e9rification d\u2019un outil de validation de transaction commerciales<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n\n        <\/div>\n    <\/div>\n<\/section>\n\n\n<section class=\"tuiles\">\n    <div class=\"container\">\n                <div class=\"bloc\">\n            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Prerequisites<\/h2>\n            <ul>\n<li>Maitrise de la programmation.<\/li>\n<li>Connaissances de base en logique.<\/li>\n<\/ul>\n\n                    <\/div>\n            <\/div>\n<\/section>\n\n\n\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Bibliography<\/h2>\n                        <ul>\n<li><a href=\"http:\/\/people.irisa.fr\/Thomas.Genet\/ACF\/\" target=\"_blank\" rel=\"noopener\">La page du cours Analyse et conception formelle par Thomas Genet<\/a><\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01208577v5\/document\" target=\"_blank\" rel=\"noopener\">A short Isabelle\/HOL tutorial for the Functional Programmer by Thomas Genet, 2017<\/a><\/li>\n<li><a href=\"https:\/\/isabelle.in.tum.de\/\" target=\"_blank\" rel=\"noopener\">L\u2019assistant \u00e0 la preuve Isabelle\/HOL, 2022<\/a><\/li>\n<li><a href=\"http:\/\/di.ulb.ac.be\/ssd\/jfr\/info-148.html\" target=\"_blank\" rel=\"noopener\">Logique pour l\u2019informatique, by Jean-Fran\u00e7ois Raskin<\/a><\/li>\n<li><a href=\"https:\/\/www.artima.com\/pins1ed\/index.html\" target=\"_blank\" rel=\"noopener\">Programming in Scala (1st edition), by Martin Odersky, Lex Spoon, and Bill Venners, 2008<\/a><\/li>\n<\/ul>\n\n        <\/div>\n    <\/div>\n<\/section>\n\n\n\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Biography<\/h2>\n                        <p><strong>Thomas Genet<\/strong> is a professor in computer science at ISTIC (Universit\u00e9 de Rennes) and a researcher in the Celtique team at IRISA. His research focuses on Verification, Term Rewriting, Tree Automata, Reachability analysis over Term Rewriting Systems, Cryptographic Protocol Verification and Blockchains and smart contract semantics.<\/p>\n\n        <\/div>\n    <\/div>\n<\/section>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":8,"featured_media":0,"parent":11707,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v20.13 - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>Software formal analysis and design - CyberSchool<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Software formal analysis and design - CyberSchool\" \/>\n<meta property=\"og:url\" content=\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/\" \/>\n<meta property=\"og:site_name\" content=\"CyberSchool\" \/>\n<meta property=\"article:publisher\" content=\"https:\/\/www.facebook.com\/CSchoolRennes\/\" \/>\n<meta property=\"article:modified_time\" content=\"2026-03-12T13:29:51+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/cyberschool.univ-rennes.fr\/app\/uploads\/2021\/02\/cover-social-network.jpeg\" \/>\n\t<meta property=\"og:image:width\" content=\"1500\" \/>\n\t<meta property=\"og:image:height\" content=\"500\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:site\" content=\"@CSchoolRennes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/\",\"url\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/\",\"name\":\"Software formal analysis and design - CyberSchool\",\"isPartOf\":{\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/#website\"},\"datePublished\":\"2023-06-08T10:42:49+00:00\",\"dateModified\":\"2026-03-12T13:29:51+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Education\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Master\u2019s and postgraduate programmes\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/\"},{\"@type\":\"ListItem\",\"position\":4,\"name\":\"Master\u2019s Cybersecurity, Science of Software and Hardware Security\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/\"},{\"@type\":\"ListItem\",\"position\":5,\"name\":\"Study programme of the Master\u2019s Cybersecurity, Science of Software and Hardware Security\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/\"},{\"@type\":\"ListItem\",\"position\":6,\"name\":\"Software formal analysis and design\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/#website\",\"url\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/\",\"name\":\"CyberSchool\",\"description\":\"Just another WordPress site\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"en-US\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Software formal analysis and design - CyberSchool","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/","og_locale":"en_US","og_type":"article","og_title":"Software formal analysis and design - CyberSchool","og_url":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/","og_site_name":"CyberSchool","article_publisher":"https:\/\/www.facebook.com\/CSchoolRennes\/","article_modified_time":"2026-03-12T13:29:51+00:00","og_image":[{"width":1500,"height":500,"url":"https:\/\/cyberschool.univ-rennes.fr\/app\/uploads\/2021\/02\/cover-social-network.jpeg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_site":"@CSchoolRennes","schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/","url":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/","name":"Software formal analysis and design - CyberSchool","isPartOf":{"@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/#website"},"datePublished":"2023-06-08T10:42:49+00:00","dateModified":"2026-03-12T13:29:51+00:00","breadcrumb":{"@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/software-formal-analysis-and-design\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/"},{"@type":"ListItem","position":2,"name":"Education","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/"},{"@type":"ListItem","position":3,"name":"Master\u2019s and postgraduate programmes","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/"},{"@type":"ListItem","position":4,"name":"Master\u2019s Cybersecurity, Science of Software and Hardware Security","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/"},{"@type":"ListItem","position":5,"name":"Study programme of the Master\u2019s Cybersecurity, Science of Software and Hardware Security","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-cybersecurity-science-of-software-and-hardware-security\/study-programme-of-the-masters-cybersecurity-science-of-software-and-hardware-security\/"},{"@type":"ListItem","position":6,"name":"Software formal analysis and design"}]},{"@type":"WebSite","@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/#website","url":"https:\/\/cyberschool.univ-rennes.fr\/en\/","name":"CyberSchool","description":"Just another WordPress site","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/cyberschool.univ-rennes.fr\/en\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"en-US"}]}},"_links":{"self":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/12126"}],"collection":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/users\/8"}],"replies":[{"embeddable":true,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/comments?post=12126"}],"version-history":[{"count":28,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/12126\/revisions"}],"predecessor-version":[{"id":18455,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/12126\/revisions\/18455"}],"up":[{"embeddable":true,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/11707"}],"wp:attachment":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/media?parent=12126"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}