{"id":20,"date":"2017-10-26T14:37:59","date_gmt":"2017-10-26T13:37:59","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=20"},"modified":"2018-05-05T04:11:56","modified_gmt":"2018-05-05T03:11:56","slug":"programme","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=20","title":{"rendered":"Programme"},"content":{"rendered":"<p>The school will cover four aspects of software verification:<\/p>\n<ul>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=44\">SMT solvers<\/a>, by <a href=\"https:\/\/members.loria.fr\/PFontaine\/\">Pascal Fontaine<\/a> (LORIA)<\/li>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=49\">Program verification with F*<\/a>, by <a href=\"https:\/\/prosecco.gforge.inria.fr\/personal\/hritcu\/\">C\u0103t\u0103lin Hri\u0163cu<\/a> (Inria Paris)<\/li>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=55\">Bounded model-checking<\/a>, by <a href=\"https:\/\/users.ecs.soton.ac.uk\/gp4\/\">Gennaro Parlato<\/a> (University of Southampton)<\/li>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=57\">Concurrent program logics<\/a>, by <a href=\"https:\/\/people.mpi-sws.org\/~viktor\/\">Viktor Vafeiadis<\/a> (MPI Kaiserslautern)<\/li>\n<\/ul>\n<p>Each topic will be covered through a long course of six hours. In addition, the school will feature four one-hour talks on more specific issues:<\/p>\n<ul>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=191#ruemmer\"><em>SMT, String and Security<\/em><\/a> by <a href=\"https:\/\/www.philipp.ruemmer.org\/\">Philipp R\u00fcmmer<\/a> (Uppsala University)<\/li>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=191#petri\"><em>Verification of invariants for convergent replicated data types<\/em><\/a> by <a href=\"https:\/\/gpetri.github.io\/\">Gustavo Petri<\/a> (Universit\u00e9 Paris Diderot)<\/li>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=191#heizmann\"><em>Traces, interpolants, and automata : Ultimate Automizer&rsquo;s approach to software verification<\/em><\/a> by <a href=\"https:\/\/swt.informatik.uni-freiburg.de\/staff\/heizmann\">Matthias Heizmann<\/a> (University of Freiburg)<\/li>\n<li><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=191#delignat\"><em>Security verification and cryptographic modelling in F*<\/em><\/a>, <a href=\"https:\/\/antoine.delignat-lavaud.fr\/\">Antoine Delignat-Lavaud<\/a> (Miscrosoft Research Cambridge)<\/li>\n<\/ul>\n<p>The <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=232\">detailed schedule<\/a> of all lectures and talks is available. A rough overview (slightly misleading) is shown below. Participants are expected to arrive on Sunday evening and leave Friday afternoon (<a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=29\">travel information<\/a>).<\/p>\n<p><center style=\"overflow:auto;\"><\/p>\n<style type=\"text\/css\">\n.smt { color: #80ab4e }\n.fstar { color: #b22 }\n.bmc { color: #bb2 }\n.cpl { color: #22b }\n.trip { opacity: 0.5 }\ntr > td:nth-child(1) { font-weight: bold }\n<\/style>\n<table class=\"tg\" border=\"0\">\n<thead>\n<tr>\n<th style=\"text-align:center;padding:1vw 0vw\"\/>\n<th style=\"text-align:center;padding:1vw 0vw\">Mon<\/th>\n<th style=\"text-align:center;padding:1vw 0vw\">Tue<\/th>\n<th style=\"text-align:center;padding:1vw 0vw\">Wed<\/th>\n<th style=\"text-align:center;padding:1vw 0vw\">Thu<\/th>\n<th style=\"text-align:center;padding:1vw 0vw\">Fri<\/th>\n<\/tr>\n<\/thead>\n<tbody>\n<tr>\n<td style=\"text-align:center;padding:1vw 0vw\">AM<\/td>\n<td class=\"smt\" style=\"text-align:center;padding:1vw 0vw\">\n    SMT 1\n  <\/td>\n<td class=\"fstar\" style=\"text-align:center;padding:1vw 0vw\">\n    F&starf; 1\n  <\/td>\n<td class=\"bmc\" style=\"text-align:center;padding:1vw 0vw\">\n    BMC 1\n  <\/td>\n<td class=\"bmc\" style=\"text-align:center;padding:1vw 0vw\">\n    BMC 2\n  <\/td>\n<td class=\"cpl\" style=\"text-align:center;padding:1vw 0vw\">\n    CPL 2\n  <\/td>\n<\/tr>\n<tr>\n<td style=\"text-align:center;padding:1vw 0vw\">PM<\/td>\n<td class=\"smt\" style=\"text-align:center;padding:1vw 0vw\">\n    SMT 2\n  <\/td>\n<td class=\"fstar\" style=\"text-align:center;padding:1vw 0vw\">\n    F&starf; 2\n  <\/td>\n<td class=\"excursion\" style=\"text-align:center;padding:1vw 0vw\">\n    Excursion\n  <\/td>\n<td class=\"cpl\" style=\"text-align:center;padding:1vw 0vw\">\n    CPL 1\n  <\/td>\n<td style=\"text-align:center;padding:1vw 0vw\"\/>\n<\/tr>\n<\/tbody>\n<\/table>\n<p><\/center><\/p>\n","protected":false},"excerpt":{"rendered":"<p>The school will cover four aspects of software verification: SMT solvers, by Pascal Fontaine (LORIA) Program verification with F*, by C\u0103t\u0103lin Hri\u0163cu (Inria Paris) Bounded model-checking, by Gennaro Parlato (University of Southampton) Concurrent program logics, by Viktor Vafeiadis (MPI Kaiserslautern) Each topic will be covered through a long course of &hellip; <\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-20","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=\/wp\/v2\/pages\/20","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=20"}],"version-history":[{"count":24,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=\/wp\/v2\/pages\/20\/revisions"}],"predecessor-version":[{"id":242,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=\/wp\/v2\/pages\/20\/revisions\/242"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=20"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}