Write a Blog >>
FormaliSE 2021
Tue 18 - Fri 21 May 2021
co-located with ICSE 2021

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 organized as a conference co-located with ICSE. The 9th edition of FormaliSE will be held on-line, co-located with ICSE 2021.

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

Tue 18 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 14:00
13:30
20m
Social Event
Platform open for social interaction
FormaliSE 2021

13:50
10m
Day opening
Welcome from the organisers
FormaliSE 2021

Media Attached
14:00 - 15:00
Property and contract specificationFormaliSE 2021 at FormaliSE Room
14:00
30m
Talk
Methodology for Specification and Verification of High-Level Properties with MetAcsl
FormaliSE 2021
Virgile Robles CEA List, Software Reliability and Security Lab, Nikolai Kosmatov CEA List, Virgile Prevosto CEA Tech List, Louis Rilling DGA Maîtrise de l'Information, Pascale Le Gall CentraleSupelec
Pre-print Media Attached
14:30
30m
Talk
How much Specification is Enough? Mutation Analysis for Software Contracts
FormaliSE 2021
Alexander Knüppel TU Braunschweig, Leon Schaer TU Braunschweig, Ina Schaefer TU Braunschweig
Media Attached
15:00 - 15:30
15:00
30m
Social Event
Platform open for social interaction
FormaliSE 2021

16:30 - 17:00
16:30
30m
Social Event
Platform open for social interaction
FormaliSE 2021

Wed 19 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 14:00
13:30
30m
Social Event
Platform open for social interaction
FormaliSE 2021

14:00 - 15:00
Model checkingFormaliSE 2021 at FormaliSE Room
14:00
30m
Talk
Formally Verified Credentials Management for Industrial Control Systems
FormaliSE 2021
Tomas Kulik Aarhus University, Jalil Boudjadar Aarhus University, Diego F. Aranha Aarhus University
Pre-print Media Attached
14:30
30m
Talk
Improved Bounded Model Checking of Timed Automata
FormaliSE 2021
Robert L. Smith Politecnico di Milano, Marcello Bersani Politecnico di Milano, Italy, Matteo Rossi Politecnico di Milano, Pierluigi San Pietro Politecnico di Milano
Pre-print Media Attached
15:00 - 15:30
15:00
30m
Social Event
Platform open for social interaction
FormaliSE 2021

17:00 - 17:30
17:00
30m
Social Event
Platform open for social interaction
FormaliSE 2021

Thu 20 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:30 - 10:00
09:30
30m
Social Event
Platform open for social interaction
FormaliSE 2021

10:00 - 11:30
Monitoring & Biological systemsFormaliSE 2021 at FormaliSE Room
10:00
30m
Talk
Monitoring Cumulative Non-functional Properties
FormaliSE 2021
Omar Al Bataineh National University of Singapore, Singapore, Arvind Easwaran Nanyang Technological University, Daniel Jun Xian Ng Nanyang Technological University, Singapore
Pre-print Media Attached
10:30
30m
Talk
Feasibility of Spatial Model Checking for Nevus Segmentation
FormaliSE 2021
Gina Belmonte Azienda Toscana Nord Ovest S. C. Fisica Sanitaria Nord, Lucca, Italy, Giovanna Broccia ISTI-CNR, FMT Lab, Vincenzo Ciancia Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo", Consiglio Nazionale delle Ricerche, Pisa, ITALY, Diego Latella ISTI-CNR, Pisa, Italy, Mieke Massink CNR-ISTI Pisa, Italy
Pre-print Media Attached
11:00
30m
Talk
Formal characterization and efficient verification of a biological robustness property
FormaliSE 2021
Lucia Nasti Università di Pisa - Dipartimento di Informatica, Roberta Gori University of Pisa, Paolo Milazzo University of Pisa - Department of Computer Science
Pre-print Media Attached
11:30 - 12:00
11:30
30m
Social Event
Platform open for social interaction
FormaliSE 2021

Fri 21 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 14:00
13:30
30m
Social Event
Platform open for social interaction
FormaliSE 2021

14:00 - 15:00
14:00
60m
Keynote
Towards Formalising Sustainable Security
FormaliSE 2021
Liliana Pasquale University College Dublin & Lero
Media Attached
15:00 - 15:30
15:00
30m
Social Event
Platform open for social interaction
FormaliSE 2021

15:30 - 17:00
“North American East Coast”FormaliSE 2021 at FormaliSE Room
15:30
30m
Talk
Runtime Verification Under Access Restrictions
FormaliSE 2021
Rania Taleb PhD student, Raphael Khoury Université du Québec à Chicoutimi, Canada, Sylvain Hallé Université du Québec à Chicoutimi
Pre-print Media Attached
16:00
30m
Talk
Quantifying Faultiness: What Does It Mean to Have N Faults
FormaliSE 2021
Media Attached
16:30
30m
Talk
Checking temporal patterns of API usage without code execution
FormaliSE 2021
Erick Raelijohn University of Montreal, Michalis Famelis Université de Montréal, Houari Sahraoui Université de Montréal
Media Attached
17:00 - 17:30
17:00
30m
Social Event
Platform open for social interaction
FormaliSE 2021

Accepted Papers

Title
Checking temporal patterns of API usage without code execution
FormaliSE 2021
Media Attached
Feasibility of Spatial Model Checking for Nevus Segmentation
FormaliSE 2021
Pre-print Media Attached
Formal characterization and efficient verification of a biological robustness property
FormaliSE 2021
Pre-print Media Attached
Formally Verified Credentials Management for Industrial Control Systems
FormaliSE 2021
Pre-print Media Attached
GUIDO: Automated Guidance for the Configuration of Deductive Program Verifiers
FormaliSE 2021
Pre-print Media Attached
How much Specification is Enough? Mutation Analysis for Software Contracts
FormaliSE 2021
Media Attached
Improved Bounded Model Checking of Timed Automata
FormaliSE 2021
Pre-print Media Attached
Methodology for Specification and Verification of High-Level Properties with MetAcsl
FormaliSE 2021
Pre-print Media Attached
Monitoring Cumulative Non-functional Properties
FormaliSE 2021
Pre-print Media Attached
PEQcheck: Localized and Context-aware Checking of Functional Equivalence
FormaliSE 2021
Media Attached
Permission-Based Verification of Red-Black Trees and Their Merging
FormaliSE 2021
Pre-print Media Attached
Platform open for social interaction
FormaliSE 2021

Program Verification: a 70-Year History
FormaliSE 2021
Media Attached
Quantifying Faultiness: What Does It Mean to Have N Faults
FormaliSE 2021
Media Attached
Runtime Verification Under Access Restrictions
FormaliSE 2021
Pre-print Media Attached
Towards Formalising Sustainable Security
FormaliSE 2021
Media Attached
Welcome from the organisers
FormaliSE 2021

Media Attached

Call for Papers

Submission types

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.
  • 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: FormaliSE encourages the submissions of new research ideas in order to stimulate discussions at the conference. For the case studies, we aim at having common domains and themes, which can facilitate the exchange of ideas during the conference. While all case study subjects are accepted, we are particularly interested in the following themes: autonomous vehicles and Covid contact tracing apps.

Submission Guidelines

FormaliSE 2021 will implement the following light-weight double-blind policy: Authors of research 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 for such advertisement.

Full papers are expected to be roughly 10 pages long including all text, figures, tables, and appendices, but excluding the references (shorter papers are acceptable). However, we would like to avoid that the authors waste time fitting their papers into that 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. Research ideas papers are expected to be roughly 4 pages plus up to 1additional page of references, with the same guiding principle as for the regular papers above. All submissions must be in English and in PDF format.

Submissions must conform to the IEEE formatting instructions IEEEConference Proceedings FormattingGuidelines (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. 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.

Papers submitted to FormaliSE 2021 must not have been published elsewhere and must not be under review or submitted for review elsewhere whilst under consideration for FormaliSE 2021.

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

We would appreciate it if the authors intending to submit a paper were to inform us in advance. In particular, we invite them to submit an abstract as early as possible and, in any case, before the Abstract submission deadline below.

Selection procedure

Each paper will be reviewed by at least three program committee members. Papers will be judged on the basis of their clarity, relevance, originality, and contribution to the field.

FormaliSE 2021 will implement a light-weight rebuttal scheme: if all the reviewers of a given submission agree that a clarification from the authors regarding one 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.

Publication

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

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

Dear all,

In the name of the Program and Organising committees of FormaliSE 2021, we wish you a happy and productive 2021. Let it bring success to your projects without calling for any sacrifices in the work-life balance!

To make our contribution towards these goals, we have decided to extend the FormaliSE 2021 abstract and paper submission deadlines to 12/01 and 19/01 (AoE), respectively.

In order to be able to follow the rest of the initially planned schedule and, in particular, to be able to send out the decision notifications on the 22/02, we have decided to maintain an abstract submission deadline 3 days ahead of the paper submission one.

Please note that, for instance, “10 pages” mentioned in the CfP for full papers is a recommendation, not a limit. Our goal is the quality of the papers, so we expect a good trade-off between the length and the readability of the paper: we prefer a paper that is slightly over 10 pages but is easy to read to a paper that is strictly 10 pages but omits clarifying details or examples.

Do submit an abstract as soon as possible. Even if it is not the final version (abstracts can be updated even after the abstract submission deadline), it will give the Program Committee some indications as to what to expect.

With our best wishes for 2021,

Laura Semini and Simon Bliudze FormaliSE 2021 PC Chairs

Questions? Use the FormaliSE contact form.