Call for Papers: FORMALISE 2025

13= th International Conference on Formal Methods in Software Engineering

<= div>

27 and 28 April, 2025

co-located with<= span style=3D"font-size:11pt;font-family:'arial' , sans-serif;color:#000000= ;background-color:transparent;font-weight:400;font-style:normal;font-varian= t:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"= >ICSE2025 (April 27-May 3, 2025), Ottawa, Canada

https://= conf.researchr.org/home/Formalise-2025

Overview

Historically, formal methods academic re= search and practical software development have had limited mutual interacti= ons =E2=80=94 except possibly in specialized domains such as safety-critica= l software. In recent times, the outlook has considerably improved: on the = one hand, formal methods research has delivered more flexible techniques an= d tools that can support various aspects of the software development proces= s: from user requirements elicitation, to design, implementation, verificat= ion and validation, as well as the creation of documentation. On the other = hand, software engineering has developed a growing interest in rigorous tec= hniques applied at scale.

The FormaliSE conference series promotes work at the in= tersection of the formal methods and software engineering communities, prov= iding a venue to exchange ideas, experiences, techniques, and results. We b= elieve more collaboration between these two communities can be mutually ben= eficial by fostering the creation of formal methods that are practically us= eful and by helping develop higher-quality software.

Originally a workshop even= t, since 2018 FormaliSE has been organized as a conference co-located with = ICSE. The 13th edition of FormaliSE will also take place as a co-located co= nference of ICSE 2025.

Areas of interest include but are not limited to= :

requirem= ents formalization and formal specification;
approac= hes, methods and tools for verification and validation;
formal approaches to safety and security related issues;
analysis of performance and other non-functional properties based = on formal approaches;
scalability of formal method a= pplications
integration of formal methods within the= software development lifecycle (e.g., change management, continuous integr= ation, regression testing, and deployment)
model-bas= ed engineering approaches;
correctness-by-constructi= on approaches for software and systems engineering;
<= span style=3D"font-size:11pt;font-family:'arial' , sans-serif;color:#000000= ;background-color:transparent;font-weight:400;font-style:normal;font-varian= t:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"= >application of formal methods to specific domains, e.g., autonomous, cyber= -physical, intelligent, and IoT systems;
formal me= thods for AI-based systems (FM4AI), and AI applied in formal method approac= hes (AI4FM);
formal methods in a certification conte= xt
case studies developed/analyzed with formal appro= aches
experience reports on the application of forma= l methods to real-world problems;
guidelines to use = formal methods in practice;
usability of formal meth= ods.

Important dates:

Abstracts due: 11 November 2024
= =
Notifications: 13 Ja= nuary 2025
Camera ready copies: 5 February 2025
FormaliSE conference: 27-28 April 2025

Paper submission = guidelines
We accept papers in three categories:=

Full research= papers describing original research work and results. We encourag= e authors to include validation of their contributions by means of a case s= tudy or experiments. We also welcome research papers focusing on tool= s and tool development.
Case study papers= discussing a significant application that suggests general lessons learned= and motivates further research, or empirically validates theoretical resul= ts (such as a technique's scalability).
Research ide= as papers describing new ideas in preliminary form, in a way that = can stimulate interesting discussions at the conference, and suggest future= work.

All papers submitted to the FormaliSE 2025 conference = must be written in English, must be unpublished original work, and must not= be under review or submitted elsewhere at the time of submission. Submissi= ons must comply with the FormaliSE's lightweight double-anonymous review pr= ocess (see below).

Full research pa= pers and case study papers can take up to 10 pages including all text, figu= res, tables and appendices, but excluding references. Research ideas papers= can take up to 4 pages, plus up to 1 additional page solely for references= .

To avoid that authors waste time = fitting their papers into the stated limit at the expense of presentation c= larity, paper lengths slightly exceeding the stated limit will still be con= sidered, provided that the reviewers find that the presentation is of high = quality.

All submissions must be in PDF format and must conform t= o the IEEE conference proceedings template, specified in the IEEE Conferenc= e Proceedings Formatting Guidelines (i.e., title in 24pt font and full text= in 10pt type): https://www.ieee.org/conferences/publishing/templates.html&= nbsp;

In = LaTeX, use \documentclass[10pt,conference]{IEEEtran}= without including the compsoc or compsocconf options.

To submit a paper to For= maliSE 2025 use thisHotCRP link: https://formalise25.hotcrp.com/=

Lightweight Double-Blind Review P= rocess for Papers
As in recent editions, FormaliS= E 2025 will use a lightweight double-anonymous process. Authors must omit t= heir names and institutions from the title page, cite their own work in the= third person, and omit acknowledgments that may reveal their identity or a= ffiliation. The purpose is reducing chances of reviewer bias influenced by = the authors=E2=80=99 identities. The double-anonymous process is, however, = lightweight, which means that it should not pose a heavy burden for authors= , nor should make a paper's presentation weaker or more difficult to review= . Also, advertising the paper as part of your usual research activities (fo= r example, on your personal web-page, in a pre-print archive, by email, in = talks or discussions with colleagues) is permitted without penalties.

Paper selection
<= span style=3D"font-size:10.5pt;font-family:'arial' , sans-serif;color:#0000= 00;background-color:transparent;font-weight:400;font-style:normal;font-vari= ant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wra= p">Each paper will be reviewed by at least three program committee members = that will judge its overall quality in terms of its soundness, significance= , novelty, verifiability, and presentation clarity.
FormaliSE 2025 will adopt a lightweight response process: = if all the reviewers of a given paper agree that a clarification from the a= uthors regarding a specific question could move the paper from "borderline"= to "accept", the chairs will relay the reviewers' questions to the authors= by email, and then share their reply with the reviewers in HotCRP. The goa= l of lightweight responses is reducing the chance of random decisions= on borderline papers. Hence, they will only be used for a minority o= f submissions; most papers will not require such an author response. Nevert= heless, we would ask the corresponding authors of all submissions to make s= ure that they are available to answer questions by email upon request.

Artifact Evaluation
Reproducibility of experimental results is crucial to foster an at= mosphere of trustworthy, open, and reusable research. To improve and reward= reproducibility, FormaliSE 2025 continues its Artifact Evaluation (AE) pro= cedure. An artifact is any additional material (software, data sets, machin= e-checkable proofs, etc.) that substantiates the claims made in the paper a= nd ideally makes them fully reproducible.

Submission of an artifact is optional but encouraged for all papers= where it can support the results presented in the paper. Artifact review i= s single-anonymous (the paper corresponding to an artifact must still follo= w the double-anonymous submissions requirements) and will be conducted conc= urrently with the paper reviewing process. Artifacts will be handled by a s= eparate Artifact Evaluation Committee, and the Artifact Evaluation process = will be set up such that the anonymization of the corresponding papers will= not be compromised. Accepted papers with a successfully evaluated artefact= will be awarded the [EAPLS badges (https://eapls.org/pages/art= ifact_badges/) that apply (among "Functional", "Reusable", a= nd "Available"). Awarded badges are to be added to the camera-ready version= of the paper.

Artifacts will be as= sessed with respect to their consistency with the results presented in the = paper, their completeness, their documentation, and their ease of use. The = Artifact Evaluation will include an initial check for technical issues; aut= hors of artifacts may be contacted by email within the first two weeks afte= r artifact submission to help resolve any technical problems that prevent t= he evaluation of an artifact if necessary.

The results of an artifact evaluation will not be available to the = reviewers of the corresponding paper; hence, they will not affect the paper= 's acceptance decision. However, reviewers will know whether a paper has su= bmitted *any* artifacts; this piece of information may be taken into accoun= t to decide whether the paper should be accepted. Thus, if there are justif= iable reasons why a paper's artifacts cannot be submitted, they should be p= ointed out in the paper so that the reviewers can appreciate them and adjus= t their expectations accordingly.

D= etailed guidelines for preparation and submission of artifacts will be desc= ribed in a dedicated page inFormaliSE 2025's website.=

Publication
All ac= cepted papers are published as part of the ICSE 2025 Proceedings in the ACM= and IEEE Digital Libraries.

At lea= st one author of each accepted paper is required to register for the confer= ence and present the paper at the conference =E2=80=94 physically or, if th= e circumstances do not allow so, virtually. Failure to register an author w= ill result in a paper being removed from the proceedings.

General Chairs

Stefania Gnesi, Istituto di Scienza e Tecnologie dell=E2=80=99Inform= azione, Italy

Nico Plat, Thanos, The Netherlands

Progra= m Chairs

Anast= asia Mavridou, KBR / NASA Ames Research Center, USA
<= span style=3D"font-size:11pt;font-family:'arial' , sans-serif;color:#000000= ;background-color:transparent;font-weight:400;font-style:normal;font-varian= t:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"= >Gwen Sala=C3=BCn, University Grenoble Alpes, France

Artifact Evaluation Chair= s

=C3=81kos Ha= jdu, Meta, UK
Lina Marsso, University of Toronto, Ca= nada

<= span style=3D"font-size:11pt;font-family:'arial' , sans-serif;color:#000000= ;background-color:transparent;font-weight:bold;font-style:normal;font-varia= nt:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap= ">Social Media Chair

Quentin Nivon, University Grenoble Alpes, France

Program committee

Bernhard Aichernig= , TU Graz, Austria
Toshiaki Aoki, Japan Advanced Ins= titute of Science and Technology, Japan
Kyungm= in Bae, Pohang University of Science and Technology, Korea
=
Domenico Bianculli, University of Luxembourg, Luxembourg =
Simon Bliudze, INRIA Lille - Nord Europe, France
Giovanna Broccia, ISTI - CNR, Italy

Radu Calinescu, University of York, UK

Pa= blo Castro, National University of Rio Cuarto, Argentina

Zhenbang Chen, NUDT, China

Nancy Day, Un= iversity of Waterloo, Canada

Francisco Dur=C3=A1n, U= niversity of M=C3=A1laga, Spain

Marie Farrell, Unive= rsity of Manchester, UK

Carlo A. Furia, USI Lu= gano, Switzerland

Fatemeh Ghassemi= , University of Tehran, Iran

Divya Gopinath, K= BR/ NASA Ames Research Center, USA

Yann-Ga= =C3=ABl Gu=C3=A9h=C3=A9neuc, Concordia University, Canada

Paula Herber, University of M=C3=BCnster, Germany

Marieke Huisman, University of Twente, The Netherlands

Fuyuki Ishikawa, National Institute of Informatics, Japa= n

Xiaoqing Jin, Apple Inc., USA

Violet Ka I Pun, Western Norway University of Applied Sciences, No= rway

Oleksandr Kolchyn, Glushkov Institute of Cybern= etics, Ukraine

Ant=C3=B3nia Lopes, University = of Lisbon, Portugal

Larissa Meinicke, Universi= ty of Queensland, Australia

Camilo Rocha, Pont= ificia Universidad Javeriana, Colombia

Cristina Sece= leanu, M=C3=A4lardalen University, Sweden

Arpi= t Sharma, EECS Department, IISER Bhopal, India

<= span style=3D"font-size:11pt;font-family:'arial' , sans-serif;color:#000000= ;background-color:transparent;font-weight:400;font-style:normal;font-varian= t:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"= >Allison Sullivan, University of Texas, Arlington, USA

Heike Wehrheim, University of Oldenburg, Germany