FormaliSE 2023
Dates to be announced Melbourne, Australia
co-located with ICSE 2023

The software industry has a long-standing and well-earned reputation for failing to deliver high-quality software. Much progress has been achieved from the early days of software development; still, nowadays, even considering the state of the art of the technologies used, the success of software projects is often not guaranteed. Many of the approaches used for developing large, complex software systems are still not able to ensure the correct behavior — and the general quality — of the delivered product, despite the efforts of the (often very qualified and skilled) software engineers involved. This is where formal methods can play a significant role. Indeed, they have been developed to provide the means for greater precision and thoroughness in modeling, reasoning about, validating, and documenting the various aspects of software systems during their development. When carefully applied, formal methods can aid all aspects of software creation: user requirement formulation, design, implementation, verification/testing, and the creation of documentation.

After decades of research though, and despite significant advancement, formal methods are still not widely used in industrial software development. We believe that a closer integration of formal methods in software engineering can help increase the quality of software applications, and at the same time highlight the benefits of formal methods in terms also of the generated return on investment (ROI).

The main objective of the conference is to foster the integration between the formal methods and the software engineering communities, to strengthen the — still too weak — links between them, and to stimulate researchers to share ideas, techniques, and results, with the ultimate goal to propose novel solutions to the fraught problem of improving the quality of software systems.

Originally a successful satellite workshop of ICSE, since 2018 FormaliSE is organised as a conference co-located with ICSE.

Areas of interest include but are not limited to:

  • Approaches and tools for verification and validation;
  • Application of formal methods to specific domains, e.g., autonomous, cyber-physical, intelligent, and IoT systems;
  • Scalability of formal methods applications;
  • Integration of formal methods within the software development lifecycle (e.g., change management, continuous integration and deployment);
  • Requirements formalization and formal specification;
  • Model-based software engineering approaches;
  • Performance analysis based on formal approaches;
  • Formal methods in a certification context;
  • Formal approaches for safety and security-related issues;
  • Usability of formal methods;
  • Guidelines to use formal methods in practice;
  • Case studies developed/analyzed with formal approaches;
  • Experience reports on the application of formal methods to real-world problems.
Dates
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 14 May

Displayed time zone: Hobart change

09:00 - 10:30
Opening / KeynoteFormaliSE 2023 at Meeting Room 102
Chair(s): Toby Murray University of Melbourne
09:00
15m
Day opening
Opening
FormaliSE 2023

09:15
75m
Keynote
Leakage Logic for programs
FormaliSE 2023
Annabelle McIver Macquarie University
11:00 - 12:30
Synthesis and AIFormaliSE 2023 at Meeting Room 102
Chair(s): Mark Utting The University of Queensland
11:00
30m
Talk
Goal Controller Synthesis for Self-Adaptive Systems
FormaliSE 2023
Radu Calinescu University of York, UK, Genaína Nunes Rodrigues University of Brasília
11:30
30m
Paper
Verifying Binary Neural Networks on Continuous Input Space using Star Reachability
FormaliSE 2023
Mykhailo Ivashchenko University of Nebraska-Lincoln, Sung Woo Choi , Luan Nguyen University of Pennsylvania, Hoang-Dung Tran Vanderbilt University
12:00
30m
Paper
Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning
FormaliSE 2023
Marcello Bersani Politecnico di Milano, Italy, Matteo Camilli Politecnico di Milano, Livia Lestingi DEIB, Politecnico di Milano, Raffaela Mirandola Politecnico di Milano, Matteo Rossi Politecnico di Milano
13:45 - 15:15
SpecificationFormaliSE 2023 at Meeting Room 102
Chair(s): Larissa A. Meinicke The University of Queensland
13:45
30m
Paper
Contract-Based Specification Refinement and Repair for Mission Planning
FormaliSE 2023
Piergiuseppe Mallozzi UC Berkeley, Inigo Incer University of California, Berkeley, Pierluigi Nuzzo University of Southern California, Alberto L. Sangiovanni-Vincentelli University of California at Berkeley, USA
14:15
30m
Paper
Patch Specifications via Product Programs
FormaliSE 2023
Cristian Cadar Imperial College London, UK, Daniel Schemmel Imperial College London, Arindam Sharma Imperial College London
14:45
30m
Paper
An Empirical Study Assessing Software Modeling in Alloy
FormaliSE 2023
Niloofar Mansoor University of Nebraska-Lincoln, Hamid Bagheri University of Nebraska-Lincoln, Eunsuk Kang Carnegie Mellon University, Bonita Sharif University of Nebraska-Lincoln, USA
15:45 - 17:15
TestingFormaliSE 2023 at Meeting Room 102
Chair(s): Cristian Cadar Imperial College London, UK
15:45
30m
Paper
Mutant Equivalence as Monotonicity in Parametric Timed Games
FormaliSE 2023
Davide Basile Formal Methods and Tools lab, ISTI-CNR, Pisa, Italy, Maurice ter Beek ISTI-CNR, Pisa, Italy, Hendrik Göttmann Technical University of Darmstadt, Malte Lochau University of Siegen
16:15
30m
Paper
Differential Testing of a Verification Framework for Compiler Optimizations (Case Study)
FormaliSE 2023
Mark Utting The University of Queensland, Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland
16:45
30m
Paper
Formalizing Symbolic Execution Path Explosion for Recursive Functions via Asymptotic Path Complexity
FormaliSE 2023
Eli Pregerson Harvey Mudd College, Shaheen Cullen-Baratloo Harvey Mudd College, David Chen Harvey Mudd College, Duy Lam Harvey Mudd College, Max Szostak Harvey Mudd College, Lucas Bang Harvey Mudd College

Mon 15 May

Displayed time zone: Hobart change

09:00 - 10:30
KeynoteFormaliSE 2023 at Meeting Room 102
Chair(s): Stefania Gnesi Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
09:15
75m
Keynote
Exploiting incompleteness in software development
FormaliSE 2023
Paola Spoletini Kennesaw State University
11:00 - 12:30
ConcurrencyFormaliSE 2023 at Meeting Room 102
Chair(s): Domenico Bianculli University of Luxembourg
11:00
30m
Paper
A Dafny-based approach to thread-local information flow analysis
FormaliSE 2023
Graeme Smith The University of Queensland
11:30
30m
Paper
Transparent Actor Model
FormaliSE 2023
Fatemeh Ghassemi University of Tehran, Marjan Sirjani Malardalen University, Ehsan Khamespanah University of Tehran, Mahrokh Mirani Tehran Institute for Advanced Studies, Hossein Hojjat Tehran Institute for Advanced Studies
12:00
30m
Paper
Using cylindric algebra to support local variables in rely/guarantee concurrency
FormaliSE 2023
Larissa A. Meinicke The University of Queensland, Ian J. Hayes The University of Queensland
13:45 - 15:15
ApplicationFormaliSE 2023 at Meeting Room 102
Chair(s): Graeme Smith The University of Queensland
13:45
30m
Paper
A Formal Approach to the Verification of Protection Systems in Low-Voltage Distribution Grids
FormaliSE 2023
Ahmed Nagy Abdelkhalek Mansour Politecnico di Milano, Samuele Grillo Politecnico di Milano, Enrico Ragaini ABB italy, Matteo Rossi Politecnico di Milano
14:15
30m
Paper
A Verified UAV Flight Plan Generator
FormaliSE 2023
Baptiste Pollien ISAE-SUPAERO, Christophe Garion ISAE-SUPAERO, Gautier Hattenberger ENAC, Pierre Roux ONERA, ISAE, Xavier Thirioux ISAE-SUPAERO
15:45 - 17:15
14:45
30m
Day closing
Closing
FormaliSE 2023

Not scheduled yet

Not scheduled yet
Lunch
Lunch
FormaliSE 2023

Not scheduled yet
Coffee break
Coffee break
FormaliSE 2023

Accepted Papers

Title
A Dafny-based approach to thread-local information flow analysis
FormaliSE 2023
A Formal Approach to the Verification of Protection Systems in Low-Voltage Distribution Grids
FormaliSE 2023
An Empirical Study Assessing Software Modeling in Alloy
FormaliSE 2023
A Verified UAV Flight Plan Generator
FormaliSE 2023
Closing
FormaliSE 2023

Coffee break
FormaliSE 2023

Contract-Based Specification Refinement and Repair for Mission Planning
FormaliSE 2023
Differential Testing of a Verification Framework for Compiler Optimizations (Case Study)
FormaliSE 2023
Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning
FormaliSE 2023
Exploiting incompleteness in software development
FormaliSE 2023
Formalizing Symbolic Execution Path Explosion for Recursive Functions via Asymptotic Path Complexity
FormaliSE 2023
Goal Controller Synthesis for Self-Adaptive Systems
FormaliSE 2023
Leakage Logic for programs
FormaliSE 2023
Lunch
FormaliSE 2023

Mutant Equivalence as Monotonicity in Parametric Timed Games
FormaliSE 2023
Opening
FormaliSE 2023

Patch Specifications via Product Programs
FormaliSE 2023
Transparent Actor Model
FormaliSE 2023
Using cylindric algebra to support local variables in rely/guarantee concurrency
FormaliSE 2023
Verifying Binary Neural Networks on Continuous Input Space using Star Reachability
FormaliSE 2023

Call for Papers

Overview

The software industry has a long-standing and well-earned reputation for failing to deliver high-quality software. Despite major advances since the early days of software development, employing the state of the art of the technologies still does not guarantee the success of software projects. Many of the approaches used for developing large, complex software systems are incapable to ensure the correct behavior — and the general quality — of the delivered product, even when the involved, often very qualified and skilled software engineers make a big effort. This is where formal methods (FMs) can play a significant role. Indeed, they have been developed to provide the means for greater precision and thoroughness in modeling, reasoning about, validating, and documenting the various aspects of software systems during their development. When carefully applied, formal methods can aid with all aspects of software creation: user requirement formulation, design, implementation, verification/testing, and the creation of documentation.

After decades of research with significant advancement, formal methods are though not yet widely used in industrial software development. We believe that a closer integration of formal methods in software engineering can help increase the quality of software applications, and at the same time highlight the benefits of formal methods in terms also of the generated return on investment (ROI).

The main objective of the conference is to foster the integration between the formal methods and the software engineering communities, to strengthen the — still too weak — links between them, and to stimulate researchers to share ideas, techniques, and results, with the ultimate goal to propose novel solutions to the fraught problem of improving the quality of software systems.

Originally a successful satellite workshop of ICSE, since 2018 FormaliSE is organized as a conference co-located with ICSE. The 11th edition of FormaliSE will also be held co-located with ICSE 2023.

Topics of Interest

Area of interest (include but are not limited to):

  • requirements formalization and formal specification;
  • approaches, 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 applications
  • integration of formal methods within the software development lifecycle (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 (FM4AI), and AI applied in formal method approaches (AI4FM);
  • formal methods in a certification context
  • case studies developed/analyzed with formal approaches
  • experience reports on the application of formal methods to real-world problems;
  • guidelines to use formal methods in practice;
  • usability of formal methods;

Important Dates

  • Abstracts due: 16 January 2023 (extended!)
  • Submissions due: 27 January 2023 (extended!)
  • Artifact registration: 27 January 2023 (extended!)
  • Artifact submissions due: 31 January 2023 (extended!)
  • Notifications: 21 February 2023
  • Camera-ready copies: 13 March 2023
  • FormaliSE conference: 14-15 May 2023

Paper Submission Guidelines

We invite you to submit:

  • Full research papers that must describe authors’ original research work and results. We encourage authors to include validation with respect to a case study in the recommended themes. We welcome research papers focusing on tools and tool development.
  • Case study papers that should identify lessons learned, validate theoretical results (such as scalability of methods) or provide specific motivation for further research and development.
  • Research ideas papers: FormaliSE encourages the submissions of new research ideas in order to stimulate discussions at the conference.

All papers submitted to the FormaliSE 2023 conference must be written in English, must be unpublished original work, and should not be under review or submitted elsewhere whilst being under consideration for FormaliSE 2023. Upon submission, papers must comply with the FormaliSE’s lightweight double-blind review process (see below).

Full research papers and case study papers are expected to be up to 10 pages long including all text, figures, tables and appendices, but excluding the references, while research ideas papers are expected to be up to 4 pages plus up to 1 additional page of references.

To avoid that authors waste time fitting their papers into the stated limit at the expense of presentation clarity, paper lengths slightly exceeding the stated limit will be tolerated provided that the presentation is of high quality, which will be left at the appreciation of the reviewers.

All submissions must be in PDF format and must conform to the IEEE Conference Proceedings Formatting Guidelines (title in 24pt font and full text in 10pt type, LaTeX users must use \documentclass[10pt,conference]{IEEEtran} without including the compsoc or compsocconf options). For details visit the IEEE templates page

Additionally, we recommend placing the following two lines in your LaTeX source right after the \documentclass command:

\usepackage[switch,columnwise]{lineno}
\linenumbers

This adds line numbers, thereby allowing reviewers to refer to specific lines in their comments.

Submissions to FormaliSE 2023 that meet the above requirements can be made via EasyChair by the submission deadline.

Lightweight Double-Blind Review Process for Papers

FormaliSE 2023 will continue to use the following light-weight double-blind process: Authors of papers must omit their names and institutions from the title page, they should refer to their other work in the third person, and omit acknowledgments that could reveal their identity or affiliation. The purpose is to avoid any bias based on authors’ identity characteristics, such as gender, seniority, or nationality, in the review process. Our goal is to facilitate an unbiased approach to reviewing by supporting reviewers’ access to works that do not carry obvious references to the authors’ identities. As mentioned above, this is a light-weight double-blind process. Anonymization should not be a heavy burden for authors and should not make papers weaker or more difficult to review. Advertising the paper on alternate forums (e.g., on a personal web-page, pre-print archive, email, talks, discussions with colleagues) is permitted, and authors will not be penalized by for such advertisement.

Paper Selection

Each paper will be reviewed by at least three program committee members that judge the paper based on its clarity, relevance, originality, and contribution to the field.

FormaliSE 2023 will continue the light-weight rebuttal scheme: if all the reviewers of a given submission agree that a clarification from the authors regarding a specific question could move a borderline paper into the acceptable range, the chairs will ask that question to the authors by e-mail and post their reply on EasyChair for the benefit of the reviewers. The goal of such light-weight rebuttals is to eliminate “coin-toss” decisions on borderline papers. Hence, it will clearly concern only a minority of submissions and most of the authors should not expect to receive such questions. However, we would ask the corresponding authors of all submissions to make sure that they are available to answer a question by email if the necessity were to arise.

Artifact Evaluation

Reproducibility of experimental results is crucial to foster an atmosphere of trustworthy, open, and reusable research. To improve and reward reproducibility, FormaliSE 2023 continues its Artifact Evaluation (AE) procedure. An artifact is any additional material (software, data sets, machine-checkable proofs, etc.) that substantiates the claims made 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. Artifact review is single-blind (the paper corresponding to an artifact must still follow the double-blind 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 Evaluation process will be set up such that the anonymization of the corresponding papers will not be compromised. The results of the evaluation may be taken into consideration for the corresponding paper acceptance decision. Accepted papers with a successfully evaluated artifact will receive a badge to be shown on the published paper’s title page.

Artifacts will be assessed 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; authors of artifacts may be contacted by e-mail within the first two weeks after artifact submission to help resolve any technical problems that prevent the evaluation of an artifact if necessary.

Detailed guidelines for preparation and submission of artifacts will be specified on a dedicated web page reachable via the artifact page on the FormaliSE 2023 website.

Publication

All accepted papers are published as part of the ICSE 2023 Proceedings in the ACM and IEEE Digital Libraries.

At least one author of each accepted paper is required to register for the conference and present the paper at the conference — physically or, if the circumstances warrant so, virtually. Otherwise, the paper will be removed from the proceedings.

Organization

General Chairs

Stefania Gnesi, Istituto di Scienza e Tecnologie dell’Informazione (Italy)

Nico Plat, University of Twente (The Netherlands)

Program Chairs

Marie-Christine Jakobs, TU Darmstadt (Germany)

Toby Murray, University of Melbourne (Australia)

Artifact Evaluation Chair

Alessio Ferrari, CNR-ISTI (Italy)

Social Media/Web Chair

Giovanna Broccia, ISTI-CNR (Italy)

Program Committee

Toshiaki Aoki, JAIST (Japan)

Ebru Aydin Gol, Middle East Technical University (Turkey)

Kyungmin Bae, Pohang University of Science and Technology (South Korea)

Simon Bliudze, INRIA Lille (France)

Ana Cavalcanti, University of York (UK)

Nancy Day, University of Waterloo (Canada)

Rayna Dimitrova, CISPA (Germany)

Gidon Ernst, LMU Munich (Germany)

Carlo A. Furia, Università della Svizzera italiana (USI) (Switzerland)

Marcus Gerhold, University of Twente (The Netherlands)

Ákos Hajdu, Facebook (UK)

Arnd Hartmanns, University of Twente (Netherlands)

Laura Humphrey, Air Force Research Laboratory (US)

Alexander Knapp, Augsburg University (Germany)

Elisavet Kozyri, Arctic University of Norway (Norway)

Mieke Massink, CNR-ISTI Pisa (Italy)

Anastasia Mavridou, KBR / NASA Ames Research Center (US)

Hernan Melgratti, Universidad de Buenos Aires (Argentina)

Claudio Menghi, McMaster University (Canada)

Alex Potanin, Australian National University (Australia)

Matteo Rossi, Politecnico di Milano (Italy)

Gerardo Schneider, Chalmers University of Technology (Sweden)

Laura Semini, University of Pisa (Italy)

Marjan Sirjani, Malardalen University (Sweden)

Yulei Sui, University of Technology Sydney (Australia)

Nils Timm, University of Pretoria (South Africa)

Heike Wehrheim, University of Oldenburg (Germany)

Kirsten Winter, Defence Science and Technology Group / University of Queensland (Australia)

Artifact Evaluation Committee

Levente Bajczi, Budapest University of Technology and Economics (Hungary)

Bishoksan Kafle, The University of Melbourne (Australia)

Andreas Katis, KBR Inc. at NASA Ames Research Center (USA)

Livia Lestingi, Politecnico di Milano (Italy)

Sharar Ahmadi, University of Surrey (UK)

Gustavo Carvalho, Universidade Federal de Pernambuco (Brazil)

Xiao Cheng, University of Technology Sydney (Australia)

Robert Müller, University of Siegen (Germany)

Martin Tappler, Graz University of Technology (Austria)

Cedric Richter, Carl von Ossietzky University of Oldenburg (Germany)

Jaime Arias, Université Paris 13 (France)

Pedro Ribeiro, University of York (UK)

Arnab Sharma, Universität Paderborn (Germany)

Laura Bussi, University of Pisa (Italy)

Virgile Robles, CEA List, Software Reliability and Security Lab (France)

Larisa Safina, Inria - Lille Nord Europe (France)

Contact Information

We can be reached at oc@formalise.org.

FormaliSE 2023 website