Calls

CALL FOR PAPERS


FM 2023 is the 25th international symposium in a series organized by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The FM symposia have been successful in bringing together researchers and industrial users around a program of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral research. FM 2023 will be both an occasion to celebrate and a platform for enthusiastic researchers and practitioners from a diversity of backgrounds to exchange their ideas and share their experiences.

Important Dates

Abstract SubmissionSeptember 4th, 2022 23:59 AoE
Full Paper Submission(including I-Day)September 11th, 202223:59 AoE
Paper NotificationNovember 15th, 202223:59 AoE
Artefact submissionNovember 20th, 202223:59 AoE
Final VersionDecember 11th, 202223:59 AoE
ConferenceMarch 6th – 10th, 2023

Topics of Interest

FM 2023 will highlight the development and application of formal methods in a wide range of domains including trustworthy AI, software, computer-based systems, systems-of-systems, cyber-physical systems, security, human-computer interaction, manufacturing, sustainability, energy, transport, smart cities, healthcare and biology. We particularly welcome papers on techniques, tools and experiences in interdisciplinary settings. We also welcome papers on experiences of applying formal methods in industrial settings, and on the design and validation of formal method tools.

The topics of interest for FM 2023 include, but are not limited to:

Interdisciplinary formal methods: Techniques, tools and experiences demonstrating the use of formal methods in interdisciplinary settings. Formal methods in practice: Industrial applications of formal methods, experience with formal methods in industry, tool usage reports, experiments with challenge problems. The authors are encouraged to explain how formal methods overcame problems, led to improved designs, or provided new insights.

Tools for formal methods: Advances in automated verification, model checking, and testing with formal methods, tools integration, environments for formal methods, and experimental validation of tools. The authors are encouraged to demonstrate empirically that the new tool or environment advances the state of the art.

Formal methods in software and systems engineering: Development processes with formal methods, usage guidelines for formal methods, and method integration. The authors are encouraged to evaluate process innovations with respect to qualitative or quantitative improvements. Empirical studies and evaluations are also solicited.

Theoretical foundations of formal methods: All aspects of theory related to specification, verification, refinement, and static and dynamic analysis. The authors are encouraged to explain how their results contribute to the solution of practical problems with formal methods or tools.

We explicitly welcome submissions to the special FM 2023 session on “Formal methods meets AI”, which is focused on formal and rigorous modeling and analysis techniques to ensure the safety, robustness, etc. (trustworthiness) of AI-based systems.

Submission Guidelines

Papers should be original work, not published or submitted elsewhere, in Springer LNCS format, written in English, submitted through EasyChair:

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

Each paper will be evaluated by at least three members of the Programme Committee. Authors of papers reporting experimental work are strongly encouraged to make their experimental results available for use by the reviewers. Case study papers should describe significant case studies, and the complete development should be made available at the time of review. The usual criteria for novelty, reproducibility, correctness and the ability for others to build upon the described work apply. Tool papers and tool demonstration papers should explain enhancements made compared to previously published work. A tool demonstration paper need not present the theory behind the tool, but can focus on the tool’s features, how it is used, its evaluation and examples and screenshots illustrating the tool’s use. Authors of tool and tool demonstration papers should make their tools available for use by the reviewers and are highly encouraged to participate in the artefact evaluation once their paper is accepted.

We solicit various categories of papers

  • Regular Papers (max 15 pages)
  • Long tool papers (max 15 pages)
  • Case study papers (max 15 pages)
  • Short papers (max 6 pages), including tool demonstration papers.

Short papers present novel ideas (e.g., without an extensive experimental evaluation) or results that can well be presented in 6 pages. Short papers will be given short presentation slots at the conference.

All page limits do not include references and appendices.

For all papers, an appendix can provide additional material such as details on proofs or experiments. The appendix is not part of the page count and is not guaranteed to be read or taken into account by the reviewers. Thus, it should not contain information necessary for the understanding and evaluation of the presented work. Papers will be accepted or rejected in the category in which they were submitted and will not be moved between categories.

At least one author of an accepted paper is expected to present the paper at the conference as a registered participant.

Double Blind Review Process

FM 2023 will employ a double-blind review process except for (a) long tool papers and (b) short tool demonstration papers. Other short papers will be subject to a double-blind policy.

The papers submitted must not reveal the authors’ identities in any way: (a) Authors should leave out author names and affiliations from the body of their submission. (b) Authors should ensure that any citation to related work by themselves is written in third person, that is, “the prior work of XYZ” as opposed to “our prior work”. (c) Authors should not include URLs to author-revealing sites (tools, datasets). (e) You are encouraged to submit a link to a Web site or repository containing supplementary material (raw data, datasets, experiments, etc.), as long as it is blinded. The visit of such sites should not be needed to conduct the review. The PC will not necessarily consider it in the paper review process. For more information, please read How to disclose data for double-blind review and make it archived open data upon acceptance.

As an alternative to having an external link, the submission form provides an option to attach a replication package. (f) Authors should anonymize author-revealing company names but instead provide general characteristics of the organizations involved needed to understand the context of the paper. (g) Authors should ensure that paper acknowledgements do not reveal the origin of their work.

The double-blind process is “heavy”, i.e., the paper anonymity will be maintained during the reviewers’ discussion period. Authors with further questions on double-blind reviewing are encouraged to contact the PC chairs by email. Papers that do not comply with the double-blind review process will be desk-rejected.

To prevent double submissions, the chairs might compare the submissions with related conferences that have overlapping review periods. The double submission restriction applies only to refereed journals and conferences, not to unrefereed forums (e.g. arXiv.org). To check for plagiarism issues, the chairs might use external plagiarism detection software.

To facilitate double-blind reviewing, we advise the authors to postpone publishing their submitted work on arXiv or similar sites until after the notification of acceptance. However, if the authors have already published a version of their paper to arXiv or similar sites, we request authors to use a different title for their submission, so that author names are not inadvertently disclosed, e.g., via a notification on Google Scholar.

Best Paper Award

At the conference, the PC Chairs will present an award to the authors of the submission selected as the FM 2023 Best Paper.

Publication

Accepted papers will be published in the Symposium Proceedings to appear in Springer’s Lecture Notes in Computer Science. Extended versions of selected papers will be invited for publication in a special issue of a journal.

Program Committee Chairs

Marsha Chechik, University of Toronto, Canada
Joost-Pieter Katoen, RWTH Aachen University, Germany & University of Twente, the Netherlands

Program Committee

See the Program Committee here.

FM 2023 Accepted Papers

PaperAuthors
The Octatope Abstract Domain for Verification of Neural NetworksTaylor Dohmen, Stanley BakAshutosh Trivedi, Alvaro Velasquez, Piotr Wojciechowski and K. Subramani
The ScalaFix equation solverGianluca Amato and Francesca Scozzari
Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B RefinementTsutomu Kobayashi, Martin Bondu and Fuyuki Ishikawa
Energy Problems in Finite and Timed Automata with Büchi ConditionsSven Dziadek, Uli Fahrenberg and Philipp Schlehuber-Caissier
SMT Sampling via Model-Guided ApproximationMatan PeledBat-Chen Rothenberg and Shachar Itzhaky
Minimisation of Spatial Models using Branching BisimilarityVincenzo Ciancia, Jan Friso Groote, Diego LatellaMieke Massink and Erik De Vink
Efficient SMT-based Network Fault Tolerance VerificationYu Liu, Pavle Subotic, Emmanuel Letier, Sergey Mechtaev and Abhik Roychoudhury
A Coq formalization of Lebesgue Induction Principle and Tonelli’s TheoremSylvie BoldoFrancois Clement, Vincent Martin, Micaela Mayero and Houda Mouhcine
Abstract Alloy InstancesJan Oliver Ringert and Allison K. Sullivan
QMaude: quantitative specification and verification in rewriting logicRubén Rubio, Narciso Marti-Oliet, Isabel Pita and Alberto Verdejo
Monitoring the Internet ComputerDavid Basin, Daniel Stefan Dietiker, Srdjan Krstic, Yvonne-Anne Pignolet, Martin Raszyk, Joshua Schneider and Arshavir Ter-Gabrielyan
Program Semantics and Verification Technique for AI-centred ProgramsFortunat Rajaona, Ioana Boureanu, Vadim Malvone and Francesco Belardinelli
Verifying Feedforward Neural Networks for Classification in Isabelle/HOLAchim D. Brucker and Amy Stell
PFL: a Probabilistic Logic for Fault TreesStefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn and Mariëlle Stoelinga
Can we Communicate? Using Dynamic Logic to Verify Team AutomataMaurice H. ter Beek, Guillermina Cledou, Rolf Hennicker and José Proença
symQV: Automated Symbolic Verification of Quantum ProgramsFabian Bauer-Marquart, Stefan Leue and Christian Schilling
Reasoning about Promises in Weak Memory Models with Event StructuresHeike Wehrheim, Lara Bargmann and Brijesh Dongol
SMPT: A Testbed for Reachabilty Methods in Generalized Petri NetsNicolas Amat and Silvano Dal Zilio
Formalising the Prevention of Microarchitectural Timing Channels by Operating SystemsRobert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser
A Decision Diagram Operation for ReachabilitySebastiaan Brand, Thomas Bäck and Alfons Laarman
A fine-grained semantics for arrays and pointers under weak memory modelsRobert Colvin
VeyMont: Parallelising Verified Programs instead of Verifying Parallel ProgramsPetra van den Bos and Sung-Shik Jongmans
Verifying At the Level of Java BytecodeMarco Paganoni and Carlo A. Furia
A Runtime Environment for Contract AutomataDavide Basile and Maurice H. ter Beek
Tableaux for Realizability of Safety SpecficationsMontserrat Hermo, Paqui Lucio and Cesar Sanchez
HHLPy: Practical Verification of Hybrid Systems using Hoare LogicHuanhuan Sheng, Alexander Bentkamp and Bohua Zhan
Word Equations in Synergy with Regular ConstraintsFrantišek Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš HolíkOndrej Lengal and Juraj Síč
Railway Scheduling Using Boolean Satisfiability Modulo SimulationsTomáš Kolárik and Stefan Ratschan

CALL FOR ARTEFACT EVALUATION


FM 2023 will include an artefact evaluation (AE) for the first time this year.

An artefact is any additional material such as software, data sets, log files, machine-checkable proofs, etc. that substantiates the claims made in the paper. Ideally, the artefact allows to fully reproduce all results in the corresponding paper by providing details on all relevant steps, inputs, configurations and parameters used. For tools, an artefact typically consists of the source code or binary of the tool as well as corresponding documentation on how to use it – and ideally also extend it.

For all accepted FM papers, authors can submit an artefact substantiating the claims of the paper. Note that participation in the AE is optional, but we strongly encourage participation, in particular for tool papers.

Evaluation Criteria

The primary goal of the artefact evaluation is to provide positive feedback to the authors and in particular reward and encourage replicable research. The AE takes place for the first time this year and we are aware that the timeline is rather short. We therefore strive to offer a low entry hurdle for artefacts and reward authors of successful artefacts with a badge that can be shown on the title page of the accepted paper.

The artefact evaluation committee will evaluate submitted artefacts with respect to two main criteria: availability and reproducibility:

  • artefact available: the artefact is publicly available on a permanent storage (for example on Zenodo).
  • artefact reproducible: the claims and results in the corresponding paper can be reproduced using the artefact.

Submission guidelines

The artefact submission is handled via EasyChair. Select the FM 2023 Artefact Evaluation track and provide the following information:

  1. Artefacts should have the same title and authors as the accepted paper.
  2. The (short) abstract should summarize the content of the artefact and explains the relation to the paper. In particular the abstract should:
    • provide an URL (preferably a DOI) to a publicly available zip file containing the artefact and all relevant files. We recommend to use Zenodo for hosting the artefact.
    • SHA256 checksum of the zip file (to ensure consistency). The checksum can be generated with:
      • Linux: sha256sum <file>
      • Windows: CertUtil -hashfile <file> SHA256
      • MacOS: shasum -a 256 <file>
    • (if required) special requirements for running the artefact (specific hardware or software, number of cores, etc.)
    • if you are aiming for the reproducible badge: Clearly state which parts of the paper should be reproducible and how they can be reproduced (for example using specific scripts or following step-by-step instructions given in the artefact README). If part of the results cannot be reproduced, shortly explain why this is the case.
  3. Please also upload a PDF file of the accepted paper.

Artefact guidelines

The artefact on the permanent storage (e.g. Zenodo) should be based on a virtual machine (VM) image or a docker image.
The artefact should contain:

  • A file License.txt containing the license for the artefact. The license must at least allow the Artefact Evaluation Committee to evaluate the artefact w.r.t. the criteria mentioned above.
  • A README file containing step-by-step instructions on how to use the artefact. In addition, please document in step-by-step instructions, how to reproduce the results of the paper using the artefact.
  • all code, binaries, example files, documentation, scripts, etc. required to reproduce the results in the paper.

Suggestions for preparing the artefact

In the following, we list some general suggestions for preparing the artefact:

  • In case of a VM image, please use VirtualBox and save the VM image as an Open Virtual Appliance (OVA) file.
  • When writing step-by-step instructions, assume minimum expertise of users.
  • Keep the replication simple through easy-to-use scripts and detailed instructions.
  • The artefact should run out of the box and not require the user to install any additional software. All required packages should already be provided in the VM image or Docker image.
  • For experiments that require a large amount of resources (time, memory, etc.), it is recommended to indicate a subset of the results of the paper which can be reproduced with reasonably modest resources (w.r.t. RAM, number of cores, etc.) and in a reasonable amount of time. Please also include the full set of experiments (for reviewers with sufficient hardware or time), just make it optional.
  • In case the artefact cannot comply with some of the guidelines, please do not hesitate to contact the AE chair (m.volk@utwente.nl) before the AE submission deadline. An example is restrictively-licensed software such as Matlab.

Timeline

(all times are 23:59 AoE)

  • Nov. 20th: Artefact submission deadline
  • until Nov. 27th: Communication period with authors in case of technical issues with the artefact
  • Dec. 7th: Author notification of AE reviews
  • Dec. 11th: Final version of the accepted paper (including possible AE badges)

Artefact Evaluation Committee

Chair Affiliation
Matthias VolkUniversity of Twente, NL
MembersAffiliation
Roman AndriushchenkoBrno University of Technology, CZ
Cesar CornejoUniversity of Rio Cuarto, AR
Federico FormicaMcMaster University, CA
Ritam GangulyMichigan State University, US
Lutz KlinkenbergRWTH Aachen University, DE
Anik MomtazMichigan State University, US
Luciano PutrueleUniversity of Rio Cuarto, AR
Marco ScalettaTU Darmstadt, DE
SoaibuzzamanBauhaus-Universität Weimar, DE
Gerard TaboneUniversity of Malta, MT
Yiming XuAustralian National University, AU

CALL FOR WORKSHOPS AND TUTORIALS


We are inviting proposals for workshops, tutorials (and other similar events) that will complement the main FM 2023 symposium. We encourage a diversity of topics relating to different ways of developing and using formal methods. Due to the growing interest in AI and machine learning-based software development, we particularly invite topics at the intersection of machine learning and formal methods.

The general purpose of workshops and tutorials is to provide an informal setting for participants to discuss technical issues, exchange research ideas and educational approaches, and to discuss and/or demonstrate applications. These may be driven by fundamental academic interests, or by needs from specific application domains.

A workshop is an event that involves an open call for contributions. A tutorial is an event based entirely on invited talks by the organizers or by invited speakers. Events that mix open and invited presentations will also be considered.

Workshops and tutorials will take place on March 6th & 10th, 2023, flanking the main symposium. Each event (workshop or tutorial) should typically run for a half day or one day, but two-day events will also be considered. The FM 2023 organizing committee aims to contribute to at least partial support for one invited speaker per event.

Submission Information

Researchers and practitioners wishing to organize a workshop or tutorial are invited to submit proposals by e-mail to the Workshops & Tutorials Chairs:

Tutorial chairs:

  • Cesar Sanchez (cesar.sanchez@imdea.org) and
  • Martin Sachenbacher (sachenbacher@isp.uni-luebeck.de)

Workshop chairs:

  • Esfandiar Mohammadi (esfandiar.mohammadi@uni-luebeck.de) and
  • Volker Stolz (vsto@hvl.no)

An event proposal should not exceed three pages and should include the following information:

  • Title and brief technical description of the event, specifying its goals and formal methods focus, and whether the event is a workshop, tutorial, or any other kind of event.
  • The names and contact information (web page, email address) of the organizers. The organizers of a workshop will also be its Programme Committee (PC) chairs; in this case, the proposal may also list prospective international PC members.
  • Pointers to information about past editions of the event, if applicable. Workshop proposals should specify whether it has taken place before; how often it has been co-located with FM or with other conferences, and the number of participants in the most recent installments.
  • A discussion of the proposed format and agenda (for example: paper presentations, tutorials, demo sessions, etc). The organizers are encouraged to describe their vision for an online event, should the need occur in light of the current global pandemic crisis.
  • The proposed duration: half or one day. Exceptionally, two-day events may be considered.
  • Potential invited speaker(s).
  • Workshop proposals should describe procedures for selecting papers and participants, including a tentative timeline for submission and notification of acceptance, and plans for the publication of proceedings, if any.

Important Dates

Submission of Workshop proposalsJune 10, 2022
Notification of success of proposals (Workshops)June 24, 2022
Submission of Tutorial proposalsJuly 1, 2022
Notification of success of proposals (Tutorials)July 15, 2022
Workshop/Tutorial datesMarch 6/10, 2023