TLA+ Community Event 2024
Tuesday, September 10, 2024
Milano, Italy

TLA+ Community Event 2024

Politecnico di Milano
Piazza Leonardo da Vinci
Room 3.1.7

Program

time (CEST)titlespeakeraffiliationslides
08:55Welcome & Opening AnnouncementsStephan Merz
09:00Apalache TutorialIgor Konnovpdf
09:50Verifying Liveness Properties of Consensus AlgorithmsGiuliano LosaStellar Foundationpdf
10:20Coffee Break
10:50Specifying BGP Using TLA+Aman ShaikhGooglepdf
11:40Real Animation of TLA+ ModelsMichael Leuschel & Jan GruteserHHU Düsseldorfpdf
12:30Lunch
14:00B+ or how to model system properties in a formal software model (FMICS keynote)Thierry LecomteClearsy
15:20Coffee Break
15:50Validating Traces of Distributed Programs Against TLA+ SpecificationsStephan MerzInriapdf
16:20A Model-Based Approach for the Formal Verification of SpecificationsAndrew SamokishLMF & Knowledge Insidepptx
16:50Towards TLAPS IDEKarolis PetrauskasVilnius Universitypdf
17:20On Proof Support in Event-B and TLAJean Paul Bodeveix, Mamoun Filali & Anne GrieuUniversity of Toulouse & IRITpdf
17:50End of the meeting

Co-located with FM 2024 in Milano (Italy), on September 10, 2024.

TLA+ is a language that is used in academia and industry for formally specifying systems. It is supported by verification tools, including the TLC and Apalache model checkers and the TLAPS proof system. PlusCal serves as a frontend for generating TLA+ specifications from an algorithmic language with an imperative flavor.

The TLA+ Community Event serves as a forum where practitioners and researchers interested in the use and further development of the TLA+ specification language and its tools meet and discuss.

Proposals for contributed talks are sollicited that present work of interest to users of TLA+ or PlusCal, such as:

  • industrial or academic case studies,
  • new tools for TLA+ or add-ons to existing tools,
  • innovative use of existing tools or reports on their shortcomings,
  • use of TLA+ in education.

Proposals for presentations, with a short (2 page) abstract summarizing the content, should be sent to tla2024@inria.fr by July 7, 2024. Please indicate if you want to give a short or long presentation (25 or 40 minutes, including discussion). Notification will be given by July 15, 2024.

There will not be formal proceedings, but the abstracts and presentations will be made available on the Web.

Participants will be required to register to FM 2024 (early registration deadline July 30, 2024).

Organizers

  • Igor Konnov, researcher in security and formal methods and TU Wien
  • Stephan Merz, Inria Nancy

Program committee

  • Ivan Beschastnikh, University of British Columbia
  • Julia Ferraioli, Amazon
  • Markus Kuppe, Microsoft
  • Michael Leuschel, Heinrich-Heine Universität Düsseldorf
  • Calvin Loncaric, Oracle
  • Giuliano Losa, Stellar Development Foundation