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 Submission | September 4th, 2022 | 23:59 AoE |
| Full Paper Submission(including I-Day) | September 11th, 2022 | 23:59 AoE |
| Paper Notification | November 15th, 2022 | 23:59 AoE |
| Artefact submission | November 20th, 2022 | 23:59 AoE |
| Final Version | December 11th, 2022 | 23:59 AoE |
| Conference | March 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
| Paper | Authors |
| The Octatope Abstract Domain for Verification of Neural Networks | Taylor Dohmen, Stanley Bak, Ashutosh Trivedi, Alvaro Velasquez, Piotr Wojciechowski and K. Subramani |
| The ScalaFix equation solver | Gianluca Amato and Francesca Scozzari |
| Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement | Tsutomu Kobayashi, Martin Bondu and Fuyuki Ishikawa |
| Energy Problems in Finite and Timed Automata with Büchi Conditions | Sven Dziadek, Uli Fahrenberg and Philipp Schlehuber-Caissier |
| SMT Sampling via Model-Guided Approximation | Matan Peled, Bat-Chen Rothenberg and Shachar Itzhaky |
| Minimisation of Spatial Models using Branching Bisimilarity | Vincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink and Erik De Vink |
| Efficient SMT-based Network Fault Tolerance Verification | Yu Liu, Pavle Subotic, Emmanuel Letier, Sergey Mechtaev and Abhik Roychoudhury |
| A Coq formalization of Lebesgue Induction Principle and Tonelli’s Theorem | Sylvie Boldo, Francois Clement, Vincent Martin, Micaela Mayero and Houda Mouhcine |
| Abstract Alloy Instances | Jan Oliver Ringert and Allison K. Sullivan |
| QMaude: quantitative specification and verification in rewriting logic | Rubén Rubio, Narciso Marti-Oliet, Isabel Pita and Alberto Verdejo |
| Monitoring the Internet Computer | David 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 Programs | Fortunat Rajaona, Ioana Boureanu, Vadim Malvone and Francesco Belardinelli |
| Verifying Feedforward Neural Networks for Classification in Isabelle/HOL | Achim D. Brucker and Amy Stell |
| PFL: a Probabilistic Logic for Fault Trees | Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn and Mariëlle Stoelinga |
| Can we Communicate? Using Dynamic Logic to Verify Team Automata | Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker and José Proença |
| symQV: Automated Symbolic Verification of Quantum Programs | Fabian Bauer-Marquart, Stefan Leue and Christian Schilling |
| Reasoning about Promises in Weak Memory Models with Event Structures | Heike Wehrheim, Lara Bargmann and Brijesh Dongol |
| SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets | Nicolas Amat and Silvano Dal Zilio |
| Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems | Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser |
| A Decision Diagram Operation for Reachability | Sebastiaan Brand, Thomas Bäck and Alfons Laarman |
| A fine-grained semantics for arrays and pointers under weak memory models | Robert Colvin |
| VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs | Petra van den Bos and Sung-Shik Jongmans |
| Verifying At the Level of Java Bytecode | Marco Paganoni and Carlo A. Furia |
| A Runtime Environment for Contract Automata | Davide Basile and Maurice H. ter Beek |
| Tableaux for Realizability of Safety Specfications | Montserrat Hermo, Paqui Lucio and Cesar Sanchez |
| HHLPy: Practical Verification of Hybrid Systems using Hoare Logic | Huanhuan Sheng, Alexander Bentkamp and Bohua Zhan |
| Word Equations in Synergy with Regular Constraints | František Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč |
| Railway Scheduling Using Boolean Satisfiability Modulo Simulations | Tomáš 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:
- Artefacts should have the same title and authors as the accepted paper.
- 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>
- Linux:
- (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.
- 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.txtcontaining 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 Volk | University of Twente, NL |
| Members | Affiliation |
| Roman Andriushchenko | Brno University of Technology, CZ |
| Cesar Cornejo | University of Rio Cuarto, AR |
| Federico Formica | McMaster University, CA |
| Ritam Ganguly | Michigan State University, US |
| Lutz Klinkenberg | RWTH Aachen University, DE |
| Anik Momtaz | Michigan State University, US |
| Luciano Putruele | University of Rio Cuarto, AR |
| Marco Scaletta | TU Darmstadt, DE |
| Soaibuzzaman | Bauhaus-Universität Weimar, DE |
| Gerard Tabone | University of Malta, MT |
| Yiming Xu | Australian 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 proposals | June 10, 2022 |
| Notification of success of proposals (Workshops) | June 24, 2022 |
| Submission of Tutorial proposals | July 1, 2022 |
| Notification of success of proposals (Tutorials) | July 15, 2022 |
| Workshop/Tutorial dates | March 6/10, 2023 |