Call for Papers: FORMALISE 202= 5

<= div style=3D"font-family:'arial' , 'helvetica' , sans-serif;font-size:12pt;= color:#000000">

13th International = Conference on Formal Methods in Software Engineering

27 and 28 Apri= l, 2025

co-located with ICSE 2025 (April 2= 7-May 3, 2025), Ottawa, Canada

https://conf.researchr.org/home/Form= alise-2025

Overview

Historically, formal methods academic research and practical software = development have had limited mutual interactions =E2=80=94 except possibly = in specialized domains such as safety-critical software. In recent times, t= he outlook has considerably improved: on the one hand, formal methods resea= rch has delivered more flexible techniques and tools that can support vario= us aspects of the software development process: from user requirements elic= itation, to design, implementation, verification and validation, as well as= the creation of documentation. On the other hand, software engineering has= developed a growing interest in rigorous techniques applied at scale.

The Forma= liSE conference series promotes work at the intersection of the formal meth= ods and software engineering communities, providing a venue to exchange ide= as, experiences, techniques, and results. We believe more collaboration bet= ween these two communities can be mutually beneficial by fostering the crea= tion of formal methods that are practically useful and by helping develop h= igher-quality software.

Originally a workshop event, since 2018 FormaliSE has bee= n organized as a conference co-located with ICSE. The 13th edition of Forma= liSE will also take place as a co-located conference of ICSE 2025.

Areas of inte= rest include but are not limited to:

requirements formalization and formal s= pecification;
approaches, methods and tools for veri= fication and validation;
formal approaches to safet= y and security related issues;
<= p dir=3D"ltr" style=3D"line-height:1.38;margin:0px">analysis of performan= ce and other non-functional properties based on formal approaches;
scalability of formal method applications

integration of formal methods within the software development lifecycl= e (e.g., change management, continuous integration, regression testing, and= deployment)

model-based engineering approaches;

correctness-by-construction approaches for software and= systems engineering;

application of formal methods = to specific domains, e.g., autonomous, cyber-physical, intelligent, and IoT= systems;

formal methods for AI-based systems (FM4= AI), and AI applied in formal method approaches (AI4FM);

formal methods in a certification context

case = studies developed/analyzed with formal approaches

ex= perience reports on the application of formal methods to real-world problem= s;

guidelines to use formal methods in practice;

usability of formal methods.

Important dates:

Abstracts= due: 18 November 2024 (AoE) - EXTENDED DEADLINE
Sub= missions: 25 November 2024 (AoE) - EXTENDED DEADLINE
<= 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"= >Notifications: 13 January 2025
=
Camera ready copies:= 5 February 2025
FormaliSE conference: 27-28 April 2= 025

Paper submission guidelines
We accept papers = in three categories:

Full research papers describing original research work and = results. We encourage authors to include validation of their contributions = by means of a case study or experiments. We also welcome research pap= ers focusing on tools and tool development.

Case stu= dy papers discussing a significant application that suggests gener= al lessons learned and motivates further research, or empirically validates= theoretical results (such as a technique's scalability).

Research ideas papers describing new ideas in preliminary fo= rm, in a way that can stimulate interesting discussions at the conference, = and suggest future work.

All papers submitted to the FormaliS= E 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 su= bmission. Submissions must comply with the FormaliSE's lightweight double-a= nonymous review process (see below).

To avoid that a= uthors waste time fitting their papers into the stated limit at the expense= of presentation clarity, paper lengths slightly exceeding the stated limit= will still be considered, provided that the reviewers find that the presen= tation is of high quality.

All submissions must be in PDF format = and must conform to the IEEE conference proceedings template, specified in = the IEEE Conference Proceedings Formatting Guidelines (i.e., title in 24pt = font and full text in 10pt type): https://www.ieee.org/conferences/publishi= ng/templates.html

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

To subm= it a paper to FormaliSE 2025 use thisHotCRP link: https://formal= ise25.hotcrp.com/

Lightweight Doub= le-Blind Review Process for Papers
As in recent e= ditions, FormaliSE 2025 will use a lightweight double-anonymous process. Au= thors must omit their names and institutions from the title page, cite thei= r own work in the third person, and omit acknowledgments that may reveal th= eir identity or affiliation. The purpose is reducing chances of reviewer bi= as influenced by the authors=E2=80=99 identities. The double-anonymous proc= ess is, however, lightweight, which means that it should not pose a heavy b= urden for authors, nor should make a paper's presentation weaker or more di= fficult to review. Also, advertising the paper as part of your usual resear= ch activities (for example, on your personal web-page, in a pre-print archi= ve, by email, in talks or discussions with colleagues) is permitted without= penalties.

Paper selection=
Each paper will be reviewed by at least three program c= ommittee members that will judge its overall quality in terms of its soundn= ess, significance, novelty, verifiability, and presentation clarity.=

FormaliSE 2025 will adopt a lightweight r= esponse process: if all the reviewers of a given paper agree that a clarifi= cation from the authors regarding a specific question could move the paper = from "borderline" to "accept", the chairs will relay the reviewers' questio= ns to the authors by email, and then share their reply with the reviewers i= n HotCRP. The goal of lightweight responses is reducing the chance of = random decisions on borderline papers. Hence, they will only be used= for a minority of submissions; most papers will not require such an author= response. Nevertheless, we would ask the corresponding authors of all subm= issions to make sure that they are available to answer questions by email u= pon request.

Artifact Evaluation
Reproducibility of experimental results is crucial= to foster an atmosphere of trustworthy, open, and reusable research. To im= prove and reward reproducibility, FormaliSE 2025 continues its Artifact Eva= luation (AE) procedure. An artifact is any additional material (software, d= ata sets, machine-checkable proofs, etc.) that substantiates the claims mad= e in the paper and 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. Ar= tifact review is single-anonymous (the paper corresponding to an artifact m= ust still follow the double-anonymous submissions requirements) and will be= conducted concurrently with the paper reviewing process. Artifacts will be= handled by a separate Artifact Evaluation Committee, and the Artifact Eval= uation process will be set up such that the anonymization of the correspond= ing papers will not be compromised. Accepted papers with a successfully eva= luated artefact will be awarded the [EAPLS badges (https://eapls.org/pages/artifact_badges/= ) that apply (among "Functional", "Reusable", and "Available"). Awarded= badges are to be added to the camera-ready version of the paper.

Artifacts will be assessed with respect to t= heir consistency with the results presented in the paper, their completenes= s, their documentation, and their ease of use. The Artifact Evaluation will= include an initial check for technical issues; authors of artifacts may be= contacted by email within the first two weeks after artifact submission to= help resolve any technical problems that prevent the evaluation of an arti= fact if necessary.

The results of a= n artifact evaluation will not be available to the reviewers of the corresp= onding paper; hence, they will not affect the paper's acceptance decision. = However, reviewers will know whether a paper has submitted *any* artifacts;= this piece of information may be taken into account to decide whether the = paper should be accepted. Thus, if there are justifiable reasons why a pape= r's artifacts cannot be submitted, they should be pointed out in the paper = so that the reviewers can appreciate them and adjust their expectations acc= ordingly.

Detailed guidelines for p= reparation and submission of artifacts will be described in a dedicated pag= e inFormaliSE 2025's website.

Publication
All accepted papers are publ= ished as part of the ICSE 2025 Proceedings in the ACM and IEEE Digital Libr= aries.

At least one author of each = accepted paper is required to register for the conference and present the p= aper at the conference =E2=80=94 physically or, if the circumstances do not= allow so, virtually. Failure to register an author will result in a paper = being removed from the proceedings.

General Chairs

Stefania Gnesi, Istituto di Scie= nza e Tecnologie dell=E2=80=99Informazione, Italy
Ni= co Plat, Thanos, The Netherlands

Program Chairs

Anastasia Mavridou, KBR / NASA Ames Rese= arch Center, USA
Gwen Sala=C3=BCn, University Grenob= le Alpes, France

Artifact Evaluation Chairs

=C3=81kos Hajdu, Meta, UK
<= 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"= >Lina Marsso, University of Toronto, Canada

Social Media Chair

Quentin Nivon, University Gre= noble Alpes, France

Program committee

Bernhard Aichernig, TU Graz, Austria

Toshiaki Aoki, Japan Advanced Institute of Science and Technology, Ja= pan

Kyungmin Bae, Pohang University of Scien= ce and Technology, Korea

<= p dir=3D"ltr" style=3D"line-height:1.38;margin:0px">Domenico Bianculli, U= niversity of Luxembourg, Luxembourg

Simon Bli= udze, INRIA Lille - Nord Europe, France

Giovanna Bro= ccia, ISTI - CNR, Italy

Radu Calinescu, University= of York, UK

Pablo Castro, National University= of Rio Cuarto, Argentina

Zhenbang Chen, NUDT,= China

Nancy Day, University of Waterloo, Canada

Francisco Dur=C3=A1n, University of M=C3=A1laga, Spain<= /span>

Marie Farrell, University of Manchester, UK

Carlo A. Furia, USI Lugano, Switzerland &nb= sp;

Fatemeh Ghassemi, University of Tehran, Iran&nbs= p;

Divya Gopinath, KBR/ NASA Ames Research Center, U= SA

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

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

Marieke Huisman, Universi= ty of Twente, The Netherlands

Fuyuki Ishikawa,= National Institute of Informatics, Japan

Xiao= qing Jin, Apple Inc., USA

Violet Ka I Pun, Western N= orway University of Applied Sciences, Norway

Oleksan= dr Kolchyn, Glushkov Institute of Cybernetics, Ukraine

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

Larissa Meinicke, University of Queensland, Australia

Camilo Rocha, Pontificia Universidad Javeriana, Colom= bia

Cristina Seceleanu, M=C3=A4lardalen University, = Sweden

Arpit Sharma, EECS Department, IISER Bh= opal, India

Allison Sullivan, University of Te= xas, Arlington, USA

Heike Wehrheim, University of Ol= denburg, Germany