September 10th, 2024

Milan, Italy

FMTea 2024

Formal Methods Teaching Workshop

Event affiliated with FM 2024, the 26th International Symposium on Formal Methods

Proceedings published as LNCS 14939

New this year: FM Teaching Expo
The last session is a demo of FM teaching material, to foster the exchange of teaching experiences and the adoption of teaching material. FMTea speakers and any other FM participants can request a "booth" by contacting the FMTea PC Chairs. This is presentation-only, without inclusion in the proceedings. Accepted booths are in the schedule below.

Invited speaker
André Platzer, Karlsruhe Institute of Technology, Germany.

Schedule

Session Chair: Emil Sekerinski
9:00 - 9:10 Opening Remarks (Slides)
9:10 - 9:40 Soaibuzzaman, Jan Oliver Ringert. Introducing GitHub Classroom into a Formal Methods Module
9:40 - 10:10 Luca Padalino, Francesca Pia Panaccione, Francesco Santambrogio, Elisabetta Di Nitto, Matteo Rossi. An Educational Module for Temporal Features in Alloy 6
10:10 - 10:40 Gustavo Carvalho. Teaching formal methods for 10 years: reflections on theories, tools, materials, and communities (Slides)

10:40 - 11:00 Break

Session Chair: Luigia Petre
11:00 - 12:00 Invited Talk: André Platzer. The Significance of Symbolic Logic for Scientific Education (Slides)
12:00 - 12:30 Luca Negrini, Vincenzo Arceri, Luca Olivieri, Agostino Cortesi and Pietro Ferrara. Teaching through Practice: Advanced Static Analysis with LiSA

12:30 - 14:00 Lunch Break

Session Chair: Catherine Dubois
14:00 - 14:30 Dominique Méry. Checking contracts in Event-B (Slides)
14:30 - 15:00 Stefan Hallerstede, John Hatcliff, Robby. Teaching with Logika: Conceiving and Constructing Correct Software (Slides)
15:00 - 15:30 Achim D. Brucker, Diego Marmsoler. Teaching Formal Methods in Application Domains: A Case Study in Computer and Network Security

15:30 - 16:00 Break and FMTea Expo setup

16:00 - 17:30 FMTea Expo

  1. John Hatcliff, Stefan Hallerstede:
    (a) Teaching with Logika: a safety-critical subset of Scala
    (b) End-to-end formal-methods-integrated development with HAMR: a model-based development framework for AADL and SysMLv2
  2. Gustavo Carvalho: a unified overview of FMs with B
    (a) Specification (Atelier B)
    (b) Animation (ProB)
    (c) Visualisation (BMotionWeb)
    (d) Verification, refinement, and code generation (Atelier B)
  3. Soaibuzzaman, Jan Oliver Ringert:
    (a) FM4SE Exercises with Autograding on GitHub Classrooms
    (b) Formal Methods Playground

Registration
Registration details at the main FM 2024 conference site.

Objectives And Scope

Formal methods originated as a means for the rigorous construction of software systems. While formal methods are increasingly being used in industry in recent years, university curricula are not adapting at the same pace. Some existing formal methods classes interest and challenge students, whereas others fail to ignite student motivation. In particular, after the pandemic, student engagement has not returned to the status quo ante. It is thus important to develop, share, and discuss approaches to effectively teach formal methods to the next generations.

We envision this event as a one-day combination of keynote and workshop presentations, where various models of teaching are presented and explored, together with innovative approaches relevant to educators of Formal Methods in the 21st century.

Organization

FMTea'24 is organized by FME’s Teaching Committee. Our broad aim is to support a worldwide improvement in learning Formal Methods, mainly by teaching but also via self-learning. To that end, we have already gathered a list of FM courses taught worldwide (https://fme-teaching.github.io) and plan to collect other resources as well, such as FM case studies, FM inspirational papers, etc. Furthermore, the FME Teaching Committee coordinates a tutorial series held online. Tutorials are collected on the FME Teaching Committee website (https://fme-teaching.github.io/).

Program Committee

  • Leila Ribeiro (co-chair), Universidade Federal do Rio Grande do Sul, Brazil
  • Emil Sekerinski (co-chair), McMaster University, Canada
  • Erika Ábrahám, RWTH Aachen University, Germany
  • Sandrine Blazy, University of Rennes 1, France
  • Brijesh Dongol, University of Surrey, UK
  • Catherine Dubois, ENSIIE, France
  • João F. Ferreira, INESC-ID & IST, University of Lisbon, Portugal
  • Markus Kuppe, Microsoft, US
  • Thierry Lecomte, CLEARSY, France
  • Michael Leuschel, University of Düsseldorf, Germany
  • Alexandra Mendes, INESC TEC & Faculty of Engineering, University of Porto, Portugal
  • Tim Nelson, Brown University, US
  • David Pearce, ConsenSys & Victoria University of Wellington, New Zealand
  • Luigia Petre, Åbo Akademi University, Finland
  • Pierluigi San Pietro, Politecnico di Milano, Italy
  • Graeme Smith, The University of Queensland, Australia

Previous Editions

The first conference on Teaching Formal Methods, TFM 2004 (archived), took place in November 2024 in Ghent, Belgium, with proceedings published as Springer LNCS 3294.

The second International FME Conference on Teaching Formal Methods, TFM 2009, affiliated with the 16th International Symposium on Formal Methods, FM 2009, took place in November 2009 in Eindhoven, The Netherlands, with proceedings published as Springer LNCS 5846.

The third Formal Methods Teaching Workshop and Tutorial, FMTea 2019, affiliated with the 3rd World Congress on Formal Methods, FM'19, took place in October 2019 in Porto, Portugal, with proceedings as Springer LNCS 11758.

The FMTea 2021 workshop, affiliated with the 24th International Symposium on Formal Methods, FM 2021, Beijing, China, was held online in November 2021, with proceedings published as Springer LNCS 13122.

The FMTea 2023 workshop, affiliated with the 25th International Symposium on Formal Methods, FM 2023, Lübeck, was held on in March 2023, with proceedings published as Springer LNCS 13962.

Several related events focused on teaching aspects for Formal Methods were held in the 2000s:

Call for Papers

FMTea'24 invites high-quality papers reporting on opinions, approaches, and experiences related to the topic of teaching Formal Methods. We aim to attract papers detailing authors’ experiences with FM Teaching. We welcome papers discussing the successes and failures of various methods, case studies, tools, etc. As self-learning is an emerging aspect of formal methods, we appreciate experiences with online teaching, including experiences with teaching formal methods via MOOCs. A non-exhaustive list of topics of interest for the FMTea'24 workshop is below:

  • Experiences and proposals related to "traditional" and online FM learning and teaching
  • Integrating and embedding formal methods within other computer science courses
  • Integrating/embedding FM teaching/thinking within other computer science courses
  • Teaching formal methods for industry
  • Innovative learning and teaching methods, like automated grading and automated feedback using Large Language Models
  • Student projects, including group projects

Software development is transforming into a rigorous engineering discipline. Improved teaching techniques will ensure that FM is at the heart of this transformation process.

Submission Details

Each submitted paper will be reviewed by at least three PC members. All submissions must be original, unpublished, and not submitted for publication elsewhere.

The proceedings will be published in the Formal Methods Teaching series of Springer’s Lecture Notes in Computer Science, https://link.springer.com/conference/tfm. We are exploring an open-access publication and expect to make an announcement shortly.

Submissions must be in PDF format, using the Springer LNCS style files (https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines). We suggest to use the LaTeX2e package (the llncs.cls class file, available in llncs2e.zip and the typeinst.dem available in typeinst.zip as a template for your contribution). Papers should not exceed 15 pages (including references) in length. Submissions should be made using the FMTea 2024 Easychair web site:

https://easychair.org/conferences/?conf=fmtea2024

All accepted papers must be presented at the workshop. Their authors must be prepared to sign a copyright transfer statement. At least one author of each accepted paper must register to the conference by an early date, to be indicated by the FM 2024 organizers, and present the paper.

Important Dates – Updated

  • 24 May 2024: Deadline for submission of abstracts
  • 30 May 2024: Deadline for submission of papers
  • 28 June 2024: Notifications to authors
  • 19 July 2024: Deadline for camera-ready version
  • 10 September 2024: FMTea'24 Workshop

Contact

Leila Ribeiro, co-chair
Emil Sekerinski, co-chair