<div dir="ltr"><br>EPIT 2018 Software Verification Spring School<br><br>Last call for participation :<br><br>  ** Pre-registration closes on April 13th.<br>  ** Please pre-register now (it takes 1 mn),<br>  ** validate and pay later.<br><br>  ** Full program announced.<br><br>=====================================================================<br><br>  When: May 7-11, 2018<br>  Where: Centre Paul-Langevin in Aussois, France<br>  Web: <a href="https://projects.lsv.fr/epit18/">https://projects.lsv.fr/epit18/</a><br><br>=====================================================================<br><br>EPIT (École de Printemps en Informatique Théorique) is a long series<br>of Spring schools in theoretical computer science, initiated by<br>Maurice Nivat in 1973. Since then, it has covered various fields of<br>computer science, and has been a key event where young researchers<br>meet.<br><br>The theme of the 2018 school is software verification. The need for<br>software verification in our information society has been recognized<br>as early as in the ’70s and it is an ever-more-important concern<br>today. Over the past decades, it has driven exciting research<br>in various fields of theoretical computer science such as logic,<br>automata, type systems, algorithms and complexity. Recently,<br>verification techniques have seen rapid development and industrial<br>adoptions, notably following the SMT revolution.<br><br><br>The school will cover several fundamental aspects<br>of software verification through four lectures (6h each):<br><br>– SMT solvers, by Pascal Fontaine (LORIA)<br>– Program verification with F*, by Cătălin Hriţcu (Inria Paris)<br>– Bounded model-checking, by Gennaro Parlato (Uni. of Southampton)<br>– Concurrent program logics, by Viktor Vafeiadis (MPI Kaiserslautern)<br><br>and four research talks (1h each):<br><br>– SMT, String and Security, by Philipp Rümmer (Uppsala University)<br>– Verification of invariants for convergent replicated data types,<br>  by Gustavo Petri (Université Paris Diderot)<br>– Traces, interpolants, and automata :<br>  Ultimate Automizer's approach to software verification,<br>  by Matthias Heizmann (University of Freiburg)<br>– F* and security,<br>  by Antoine Delignat-Lavaud (Microsoft Research Cambridge)<br><br><br>Please find more information, e.g. regarding the venue and<br>registration, on our website:<br><br>  <<a href="https://projects.lsv.fr/epit18/">https://projects.lsv.fr/epit18/</a>>.<br><br>Pre-register immediately, and spread the word!<br><br>—<br><br>The organizers,<br>David Baelde (LSV, ENS Paris-Saclay & Inria Paris)<br>Constantin Enea (IRIF, Université Paris Diderot)<br><br></div>