Animation and exchanges in the Petri Nets community

[address@concealed]

FM 2026: Call for Papers
------------------------

May 20--22, 2026
Tokyo, Japan

FM 2026 is the 27th international symposium on Formal Methods 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 2026 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.
See https://conf.researchr.org/home/fm-2026 for further details.

The FM 2026 proceedings will appear as part of the LNCS FM subline, with 
gold open access.


## Important Dates:

Abstract Submission     November 25, 2025 23:59 AoE
Full Paper Submission   December 2, 2025 23:59 AoE
Paper Notification      January 30, 2026 23:59 AoE
Final Version           February 23, 2026 23:59 AoE
Main Conference         May 20--22, 2026


## Topics of Interest

FM 2026 will highlight the development and application of formal methods 
in a wide range of domains including trustworthy AI, computer-based 
systems, systems-of-systems, cyber-physical systems, security, 
human-computer interaction, manufacturing, sustainability, energy, 
transport, smart cities, smart contracts in blockchain, 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 2026 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 are particularly interested in submissions that apply formal methods 
on autonomous systems, including AI - and non-AI-based perception, 
decision, and control algorithms, compilers, middleware, operating 
systems, virtual machines, communication protocols, and hardware. 
Example application domains are increasingly automated vehicles, robots, 
and drones.

FM 2026 features two special tracks: one on Tests and Proofs (TAP) and 
another on Tutorials.


## Track: Tests & Proofs (TAP)

TAP promotes research in verification and formal methods that targets 
the interplay of static and dynamic analysis techniques with the 
ultimate goal of improving software and system dependability.
Research in verification has seen an increase in heterogeneous 
techniques and a synergy between the traditionally distinct areas of 
dynamic and static analysis. There is growing awareness that dynamic 
techniques such as testing and static techniques such as proving are 
complementary rather than mutually exclusive. Notable examples that 
provide evidence for the potential of a combination of static and 
dynamic analysis are counterexample generation based on symbolic 
execution, the integration of SAT/SMT-solving in model checking, or the 
combination of predicate abstraction with exhaustive enumeration. The 
verification of systems based on machine learning spurs novel 
combinations of dynamic and static analyses, e.g., property verification 
of surrogate models that are generated through testing.
TAP's scope encompasses many aspects of verification technology, 
including foundational work, tool development, and empirical research.
See https://conf.researchr.org/track/fm-2026/fm-2026-tap for further 
details.


## Track: Tutorials

The primary goal of these tutorials is to convey ideas with a focus on 
pedagogy over technical innovation. They offer a valuable platform for 
participants to discuss technical challenges, exchange research 
concepts, explore educational strategies, and demonstrate or investigate 
practical applications. Tutorials should be designed to be broadly 
accessible and pedagogically oriented, clarifying key concepts, building 
intuition, and ensuring ease of understanding. They aim to attract new 
researchers, serve as bridges to practitioners, and disseminate useful 
ideas widely. These may be driven by fundamental academic interests, or 
by needs from specific application domains.
See https://conf.researchr.org/track/fm-2026/fm-2026-tutorials for 
further details.


## Submission Guidelines

We solicit various categories of papers. Except for tutorials, which has 
a dedicated track, papers in all categories can be submitted to either 
the Research or the TAP track.

- 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
- Tutorial papers submitted to the Tutorial track (max 25 pages)

All page limits do not include references and appendices.

Papers should be original work, not published or submitted elsewhere, in 
Springer LNCS format, and written in English.

Each paper will be evaluated by at least three members of the Program 
Committee. Authors of papers reporting experimental work are strongly 
encouraged to make their experimental results available for use by the 
reviewers.

Papers submitted to the TAP track will undergo the same review process 
as other papers, by PC members with expertise in tests and proofs.

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 artifact evaluation once 
their paper is accepted.

Reviewing is single-blind.

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 will only be read at the discretion of 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.

### Proceedings

The conference proceedings will be published open access by Springer in 
the LNCS series, as part of the FM subline, with gold open access.

### Submissions

Submission link: https://easychair.org/conferences/?conf=fm2026

Authors of all accepted papers are invited to submit an artifact for 
evaluation by the FM 2026 Artifact Evaluation Committee after the paper 
notification. For long tool papers and tool demonstration papers, 
submission of an artifact is strongly encouraged.

### Best Paper Award

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

### Special Issue
Extended versions of selected papers will be invited for publication in 
the ACM Formal Aspects of Computing Journal.


## Invited Talks

We are very pleased that FM 2026 will host four keynote speeches 
delivered by distinguished experts:

- Cristian Cadar, Imperial College (UK)
  https://www.doc.ic.ac.uk/~cristic/
- Ichiro Hasuo, National Institute of Informatics (Japan)
  https://group-mmm.org/~ichiro/
- Daniel Kroening, Amazon (USA)
  https://www.kroening.com/
- Ruzica Piskac, Yale University (USA)
  https://www.cs.yale.edu/homes/piskac/

The details will be announced on the webpage.
https://conf.researchr.org/track/fm-2026/fm-2026-invited_talks


## Program Committee Chairs

- Augusto Sampaio, Universidade Federal de Pernambuco, Brazil
- Marielle Stoelinga, University of Twente, the Netherlands


## Call for Workshops

We are inviting proposals for workshops (and other similar events) that 
will complement the main FM 2026 symposium. We encourage a diversity of 
topics related to different ways of developing and using formal methods. 
We are also open to topics that are on the intersection of formal 
methods with emerging fields in computer science, such as AI and machine 
learning-based software development, cyber security, and quantum computing.

Workshops will take place on May 18 and 19, 2026, before the main 
symposium. Each workshop should typically run for a half day or one day, 
but two-day events will also be considered.

Workshop proposal deadline: October 26, 2025 23:59 AoE

See the webpage for detailed submission information.
https://conf.researchr.org/track/fm-2026/fm-2026-workshops


## Collocated Events

In addition to workshops, there will be the following events collocated 
with the FM symposium.
Important dates and submission guidelines will be announced later.

### Industry Day

The Industry Day (i-Day) is a forum organised in conjunction with FM and 
targets the industrial development and use of formal methods. The 
objective of i-Day is to bring industry to the congress, and to foster 
the important discussion about where the state of the art in formal 
methods is today, seen from an industry point of view.

### Doctoral Symposium

The FM doctoral symposium aims to provide an engaging and informal 
environment where PhD students can present and discuss their ongoing 
work, meet other students working in formal methods, and receive 
feedback and advice from experienced researchers. In addition to short 
talks followed by open group discussions, the doctoral symposium will 
also provide opportunities for PhD students to meet senior academics in 
smaller groups to informally discuss research strategies, career 
aspects, or any other topic of interest.

########################################################################