deploy: cb7ff77

2024-fm/index.html

@@ -2,7 +2,7 @@
 parent
 active"><a href=/2024-fm/>2024 - TLA+ Community Event</a></li><li data-nav-id=/2024/ title="2024 - TLA+ Conf" class=dd-item><a href=/2024/>2024 - TLA+ Conf</a></li><li data-nav-id=/2023/ title="2023 - TLA+ Community Event" class=dd-item><a href=/2023/>2023 - TLA+ Community Event</a><ul><li data-nav-id=/2023/dragoischwiderski/ title class=dd-item><a href=/2023/dragoischwiderski/></a></li><li data-nav-id=/2023/olivierconstant/ title class=dd-item><a href=/2023/olivierconstant/></a></li></ul></li><li data-nav-id=/2022/ title="2022 - TLA+ Conf" class=dd-item><a href=/2022/>2022 - TLA+ Conf</a><ul></ul></li><li data-nav-id=/202110/ title="2021 - TLA+ Tutorial" class=dd-item><a href=/202110/>2021 - TLA+ Tutorial</a></li><li data-nav-id=/2021/ title="2021 - TLA+ Conf" class=dd-item><a href=/2021/>2021 - TLA+ Conf</a><ul></ul></li><li data-nav-id=/2020/ title="2020 - TLA+ Community Event" class=dd-item><a href=/2020/>2020 - TLA+ Community Event</a></li><li data-nav-id=/2019/ title="2019 - TLA+ Conf" class=dd-item><a href=/2019/>2019 - TLA+ Conf</a><ul></ul></li><li data-nav-id=/2018/ title="2018 - TLA+ Community Event" class=dd-item><a href=/2018/>2018 - TLA+ Community Event</a><ul></ul></li><li data-nav-id=/2014/ title="2014 - TLA+ Community Event" class=dd-item><a href=/2014/>2014 - TLA+ Community Event</a><ul></ul></li><li data-nav-id=/2012/ title="2012 - TLA+ Community Event" class=dd-item><a href=/2012/>2012 - TLA+ Community Event</a></li></ul><section id=footer><h4>Contact</h4>"tla2024" \o "@" \o "tlapl.us"</section></div></nav><section id=body><div id=overlay></div><div class="padding highlightable sticky-parent"><div class=sticky-spacer><div><div id=breadcrumbs itemscope itemtype=http://data-vocabulary.org/Breadcrumb><span id=sidebar-toggle-span><a href=# id=sidebar-toggle data-sidebar-toggle><i class="fa fa-bars"></i></a></span>
 <span id=toc-menu><i class="fa fa-list-alt"></i></span>
-<span class=links><a href=/>TLA+ Community Event & Conference</a> > 2024 - TLA+ Community Event</span></div><div class=progress><div class=wrapper><nav id=TableOfContents><ul><li><ul><li><a href=#program>Program</a></li><li><a href=#co-located-with-fm-2024httpswwwfm24polimiit-in-milano-italy-on-september-10-2024>Co-located with <a href=https://www.fm24.polimi.it>FM 2024</a> in Milano (Italy), on September 10, 2024.</a></li><li><a href=#organizers>Organizers</a></li><li><a href=#program-committee>Program committee</a></li></ul></li></ul></nav></div></div></div></div><div id=body-inner><div align=right><h4><p>TLA<sup>+</sup> Community Event 2024<br>Tuesday, September 10, 2024<br>Milano, Italy<br></p></h4></div><h1 id=tla-community-event-2024>TLA+ Community Event 2024</h1><p>Politecnico di Milano<br>Piazza Leonardo da Vinci<br>Room 3.1.7</p><h3 id=program>Program</h3><table><thead><tr><th>time (CEST)</th><th>title</th><th>speaker</th><th>affiliation</th><th>slides</th></tr></thead><tbody><tr><td>08:55</td><td>Welcome & Opening Announcements</td><td><a href=https://members.loria.fr/SMerz/>Stephan Merz</a></td><td></td><td></td></tr><tr><td>09:00</td><td><a href=https://github.com/apalache-mc/apalache>Apalache</a> Tutorial</td><td><a href=https://konnov.phd>Igor Konnov</a></td><td></td><td></td></tr><tr><td>09:50</td><td>Verifying Liveness Properties of Consensus Algorithms</td><td><a href=https://www.losa.fr>Giuliano Losa</a></td><td>Stellar Foundation</td><td><a href=/2024-fm/slides-losa.pdf>pdf</a></td></tr><tr><td>10:20</td><td><em>Coffee Break</em></td><td></td><td></td><td></td></tr><tr><td>10:50</td><td>Specifying BGP Using TLA+</td><td><a href=https://www.linkedin.com/in/aman-shaikh-798b48/>Aman Shaikh</a></td><td>Google</td><td><a href=/2024-fm/slides-shaikh.pdf>pdf</a></td></tr><tr><td>11:40</td><td>Real Animation of TLA+ Models</td><td><a href=https://www.cs.hhu.de/en/research-groups/software-engineering-and-programming-languages/our-team/team/michael-leuschel>Michael Leuschel</a> & Jan Gruteser</td><td>HHU Düsseldorf</td><td></td></tr><tr><td><em>12:30</em></td><td><em>Lunch</em></td><td></td><td></td><td></td></tr><tr><td>14:00</td><td>B+ or how to model system properties in a formal software model (FMICS keynote)</td><td><a href=https://fr.linkedin.com/in/thierry-lecomte-19695b>Thierry Lecomte</a></td><td>Clearsy</td><td></td></tr><tr><td>15:20</td><td><em>Coffee Break</em></td><td></td><td></td><td></td></tr><tr><td>15:50</td><td>Validating Traces of Distributed Programs Against TLA+ Specifications</td><td><a href=https://members.loria.fr/SMerz/>Stephan Merz</a></td><td>Inria</td><td><a href=/2024-fm/slides-merz.pdf>pdf</a></td></tr><tr><td>16:20</td><td><a href=/2024-fm/samokish.pdf>A Model-Based Approach for the Formal Verification of Specifications</a></td><td>Andrew Samokish</td><td>LMF & Knowledge Inside</td><td></td></tr><tr><td>16:50</td><td>Towards TLAPS IDE</td><td><a href=http://karolis.5grupe.lt/home/>Karolis Petrauskas</a></td><td>Vilnius University</td><td><a href=/2024-fm/slides-petrauskas.pdf>pdf</a></td></tr><tr><td>17:20</td><td>On Proof Support in Event-B and TLA</td><td><a href=https://www.irit.fr/~Jean-Paul.Bodeveix/>Jean Paul Bodeveix</a>, <a href=https://www.irit.fr/~Mamoun.Filali/>Mamoun Filali</a> & Anne Grieu</td><td>University of Toulouse & IRIT</td><td></td></tr><tr><td>17:50</td><td>End of the meeting</td><td></td><td></td><td></td></tr></tbody></table><h3 id=co-located-with-fm-2024httpswwwfm24polimiit-in-milano-italy-on-september-10-2024>Co-located with <a href=https://www.fm24.polimi.it>FM 2024</a> in Milano (Italy), on September 10, 2024.</h3><p><a href=https://lamport.azurewebsites.net/tla/tla.html>TLA+</a> is a language that
+<span class=links><a href=/>TLA+ Community Event & Conference</a> > 2024 - TLA+ Community Event</span></div><div class=progress><div class=wrapper><nav id=TableOfContents><ul><li><ul><li><a href=#program>Program</a></li><li><a href=#co-located-with-fm-2024httpswwwfm24polimiit-in-milano-italy-on-september-10-2024>Co-located with <a href=https://www.fm24.polimi.it>FM 2024</a> in Milano (Italy), on September 10, 2024.</a></li><li><a href=#organizers>Organizers</a></li><li><a href=#program-committee>Program committee</a></li></ul></li></ul></nav></div></div></div></div><div id=body-inner><div align=right><h4><p>TLA<sup>+</sup> Community Event 2024<br>Tuesday, September 10, 2024<br>Milano, Italy<br></p></h4></div><h1 id=tla-community-event-2024>TLA+ Community Event 2024</h1><p>Politecnico di Milano<br>Piazza Leonardo da Vinci<br>Room 3.1.7</p><h3 id=program>Program</h3><table><thead><tr><th>time (CEST)</th><th>title</th><th>speaker</th><th>affiliation</th><th>slides</th></tr></thead><tbody><tr><td>08:55</td><td>Welcome & Opening Announcements</td><td><a href=https://members.loria.fr/SMerz/>Stephan Merz</a></td><td></td><td></td></tr><tr><td>09:00</td><td><a href=https://github.com/apalache-mc/apalache>Apalache</a> Tutorial</td><td><a href=https://konnov.phd>Igor Konnov</a></td><td></td><td><a href=/2024-fm/slides-konnov.pdf>pdf</a></td></tr><tr><td>09:50</td><td>Verifying Liveness Properties of Consensus Algorithms</td><td><a href=https://www.losa.fr>Giuliano Losa</a></td><td>Stellar Foundation</td><td><a href=/2024-fm/slides-losa.pdf>pdf</a></td></tr><tr><td>10:20</td><td><em>Coffee Break</em></td><td></td><td></td><td></td></tr><tr><td>10:50</td><td>Specifying BGP Using TLA+</td><td><a href=https://www.linkedin.com/in/aman-shaikh-798b48/>Aman Shaikh</a></td><td>Google</td><td><a href=/2024-fm/slides-shaikh.pdf>pdf</a></td></tr><tr><td>11:40</td><td>Real Animation of TLA+ Models</td><td><a href=https://www.cs.hhu.de/en/research-groups/software-engineering-and-programming-languages/our-team/team/michael-leuschel>Michael Leuschel</a> & Jan Gruteser</td><td>HHU Düsseldorf</td><td></td></tr><tr><td><em>12:30</em></td><td><em>Lunch</em></td><td></td><td></td><td></td></tr><tr><td>14:00</td><td>B+ or how to model system properties in a formal software model (FMICS keynote)</td><td><a href=https://fr.linkedin.com/in/thierry-lecomte-19695b>Thierry Lecomte</a></td><td>Clearsy</td><td></td></tr><tr><td>15:20</td><td><em>Coffee Break</em></td><td></td><td></td><td></td></tr><tr><td>15:50</td><td>Validating Traces of Distributed Programs Against TLA+ Specifications</td><td><a href=https://members.loria.fr/SMerz/>Stephan Merz</a></td><td>Inria</td><td><a href=/2024-fm/slides-merz.pdf>pdf</a></td></tr><tr><td>16:20</td><td><a href=/2024-fm/samokish.pdf>A Model-Based Approach for the Formal Verification of Specifications</a></td><td>Andrew Samokish</td><td>LMF & Knowledge Inside</td><td></td></tr><tr><td>16:50</td><td>Towards TLAPS IDE</td><td><a href=http://karolis.5grupe.lt/home/>Karolis Petrauskas</a></td><td>Vilnius University</td><td><a href=/2024-fm/slides-petrauskas.pdf>pdf</a></td></tr><tr><td>17:20</td><td>On Proof Support in Event-B and TLA</td><td><a href=https://www.irit.fr/~Jean-Paul.Bodeveix/>Jean Paul Bodeveix</a>, <a href=https://www.irit.fr/~Mamoun.Filali/>Mamoun Filali</a> & Anne Grieu</td><td>University of Toulouse & IRIT</td><td><a href=/2024-fm/slides-filali.pdf>pdf</a></td></tr><tr><td>17:50</td><td>End of the meeting</td><td></td><td></td><td></td></tr></tbody></table><h3 id=co-located-with-fm-2024httpswwwfm24polimiit-in-milano-italy-on-september-10-2024>Co-located with <a href=https://www.fm24.polimi.it>FM 2024</a> in Milano (Italy), on September 10, 2024.</h3><p><a href=https://lamport.azurewebsites.net/tla/tla.html>TLA+</a> is a language that
 is used in academia and industry for formally specifying systems. It is
 supported by <a href=https://lamport.azurewebsites.net/tla/tools.html>verification tools</a>, including the TLC and Apalache model checkers and the TLAPS proof system.
 PlusCal serves as a frontend for generating TLA+ specifications from an