Email Gateway (Sep 12 2025 at 10:06): Email Gateway (Sep 12 2025 at 10:06):From: Tsutomu Kobayashi <kobayashi.tsutomu@jaxa.jp>
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.
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
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.
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.
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.
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.
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.
The conference proceedings will be published open access by Springer in the
LNCS series, as part of the FM subline, with gold open access.
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.
At the conference, the PC Chairs will present an award to the authors of the
submission selected as the FM 2026 Best Paper.
Extended versions of selected papers will be invited for publication in the
ACM Formal Aspects of Computing Journal.
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
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 A
[message truncated]
Last updated: Sep 13 2025 at 04:22 UTC