From f6e1c3367d1eb790125ed4cec2704c58db128544 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Tue, 20 Aug 2024 13:25:56 +0200 Subject: [PATCH] updated program for 2024-FM --- content/2024-fm/_index.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/content/2024-fm/_index.md b/content/2024-fm/_index.md index 80e0a2d..7e48422 100644 --- a/content/2024-fm/_index.md +++ b/content/2024-fm/_index.md @@ -19,19 +19,19 @@ Milano, Italy
time (CEST) | title | speaker | affiliation | slides | ------|--------|---------|--------|------------| 08:55 | Welcome & Opening Announcements | [Stephan Merz](https://members.loria.fr/SMerz/) | | | -09:00 | [Apalache](https://apalache.informal.systems) Tutorial | [Igor Konnov](https://konnov.phd) | | | -10:00 | Verifying Liveness Properties of Consensus Algorithms | [Giuliano Losa](https://www.losa.fr) | Stellar Foundation | | -10:30 | *Coffee Break* | -11:00 | Specifying BGP Using TLA+ | [Aman Shaikh](https://www.linkedin.com/in/aman-shaikh-798b48/) | Google | | -11:45 | Real Animation of TLA+ Models | [Michael Leuschel](https://www.cs.hhu.de/en/research-groups/software-engineering-and-programming-languages/our-team/team/michael-leuschel) & Jan Gruteser | HHU Düsseldorf | | +09:00 | [Apalache](https://github.com/apalache-mc/apalache) Tutorial | [Igor Konnov](https://konnov.phd) | | | +09:50 | Verifying Liveness Properties of Consensus Algorithms | [Giuliano Losa](https://www.losa.fr) | Stellar Foundation | | +10:20 | *Coffee Break* | +10:50 | Specifying BGP Using TLA+ | [Aman Shaikh](https://www.linkedin.com/in/aman-shaikh-798b48/) | Google | | +11:40 | Real Animation of TLA+ Models | [Michael Leuschel](https://www.cs.hhu.de/en/research-groups/software-engineering-and-programming-languages/our-team/team/michael-leuschel) & Jan Gruteser | HHU Düsseldorf | | _12:30_ | *Lunch* | -14:00 | B+ or how to model system properties in a formal software model | [Thierry Lecomte](https://fr.linkedin.com/in/thierry-lecomte-19695b) | Clearsy | | -15:00 | Validation Traces of Distributed Programs Against TLA+ Specifications | [Stephan Merz](https://members.loria.fr/SMerz/) | Inria | | -15:30 | *Coffee Break* | -16:00 | [A Model-Based Approach for the Formal Verification of Specifications](/2024-fm/samokish.pdf) | Andrew Samokish | LMF & Knowledge Inside | | -16:30 | Towards TLAPS IDE | [Karolis Petrauskas](http://karolis.5grupe.lt/home/) | Vilnius University | | -17:00 | On Proof Support in Event-B and TLA | [Jean Paul Bodeveix](https://www.irit.fr/~Jean-Paul.Bodeveix/), [Mamoun Filali](https://www.irit.fr/~Mamoun.Filali/) & Anne Grieu | University of Toulouse & IRIT | | -17:30 | End of the meeting | +14:00 | B+ or how to model system properties in a formal software model (FMICS keynote) | [Thierry Lecomte](https://fr.linkedin.com/in/thierry-lecomte-19695b) | Clearsy | | +15:20 | *Coffee Break* | +15:50 | Validation Traces of Distributed Programs Against TLA+ Specifications | [Stephan Merz](https://members.loria.fr/SMerz/) | Inria | | +16:20 | [A Model-Based Approach for the Formal Verification of Specifications](/2024-fm/samokish.pdf) | Andrew Samokish | LMF & Knowledge Inside | | +16:50 | Towards TLAPS IDE | [Karolis Petrauskas](http://karolis.5grupe.lt/home/) | Vilnius University | | +17:20 | On Proof Support in Event-B and TLA | [Jean Paul Bodeveix](https://www.irit.fr/~Jean-Paul.Bodeveix/), [Mamoun Filali](https://www.irit.fr/~Mamoun.Filali/) & Anne Grieu | University of Toulouse & IRIT | | +17:50 | End of the meeting | ### Co-located with [FM 2024](https://www.fm24.polimi.it) in Milano (Italy), on September 10, 2024.