Write a Blog >>
ICSE 2020
Wed 24 June - Thu 16 July 2020

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 system 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. FormaliSE 2020 will take place as a virtual conference on 13 July 2020.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 13 Jul

Displayed time zone: (UTC) Coordinated Universal Time change

07:00 - 09:00
Session 1: Keynote and Q+A of paper presentationsFormaliSE at Goguryeo
07:00
60m
Talk
SYNTECH: Synthesis Technologies for Reactive Systems Software Engineers
FormaliSE
K: Shahar Maoz Tel Aviv University
08:00
60m
Live Q&A
Q&A to authors of pre-recorded paper presentations
FormaliSE

15:00 - 17:00
Session 2: Keynote and Q+A of paper presentationsFormaliSE at Goguryeo
15:00
60m
Talk
On the Probabilistic Analysis of Neural Networks
FormaliSE
K: Corina S. Pasareanu Carnegie Mellon University Silicon Valley, NASA Ames Research Center
16:00
60m
Live Q&A
Q&A to authors of pre-recorded paper presentations
FormaliSE

Unscheduled Events

Not scheduled
Paper
Rule-based Word Equation Solving
FormaliSE
Joel D. Day Loughborough University, Mitja Kulczynski Kiel University, Florin Manea University of Göttingen, Dirk Nowotka Kiel University, Danny Bøgsted Poulsen Aalborg University
Not scheduled
Paper
Minimal Assumptions Refinement for Realizable Specifications
FormaliSE
Davide Giacomo Cavezza Imperial College London, Dalal Alrajeh Imperial College London, András György DeepMind
Not scheduled
Paper
Relational Test Tables: A Practical Specification Language for Evolution and Security
FormaliSE
A: Alexander Weigl Karlsruhe Institute of Technology, A: Mattias Ulbrich Karlsruhe Institute of Technology, A: Suhyun Cha Karlsruhe Institute of Technology, A: Bernhard Beckert Karlsruhe Institute of Technology, A: Birgit Vogel-Heuser Karlsruhe Institute of Technology
Not scheduled
Paper
UML consistency rules: a case study with open-source UML models
FormaliSE
Damiano Torre University of Luxembourg, Yvan Labiche Carleton University, Marcela Fabiana Genero Bocco University of Castilla-La Mancha, Maged Elaasar Carleton University, Claudio Menghi University of Luxembourg
Not scheduled
Paper
Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study
FormaliSE
Simon Foster University of York, Yakoub Nemouchi University of York, Colin O'Halloran D-RisQ Software Systems, Karen Stephenson D-RisQ Software Systems, Nick Tudor D-RisQ Software Systems
Not scheduled
Paper
Security Analysis of a Quadruple-tank Water System via Statistical Model Checking
FormaliSE
Andrei Munteanu University of Verona, Michele Pasqua University of Verona, Massimo Merro University of Verona
Not scheduled
Paper
Verification of Privacy-Enhanced Collaborations
FormaliSE
Sara Belluccini IMT Lucca School for Advanced Studies, Rocco De Nicola IMT Institute for Advanced Studies, Marlon Dumas University of Tartu, Pille Pullonen Cybernetica AS, Barbara Re University of Camerino, Francesco Tiezzi University of Camerino
Not scheduled
Paper
Mind the gap: Robotic Mission Planning Meets Software Engineering
FormaliSE
Mehrnoosh Askarpour Politecnico di Milano, Claudio Menghi University of Luxembourg, Gabriele Belli Alten, Marcello M. Bersani Politecnico di Milano, Patrizio Pelliccione University of L'Aquila and Chalmers | University of Gothenburg
Not scheduled
Paper
Security Verification of Industrial Control Systems using Partial Model Checking
FormaliSE
Tomas Kulik Aarhus University, Jalil Boudjadar Aarhus University, Peter W. V. Tran-Jørgensen Aarhus University
Not scheduled
Paper
Semantic-based Architecture Smell Analysis
FormaliSE
Nacha Chondamrongkul School of Computer Science, the University of Auckland, Jing Sun School of Computer Science, the University of Auckland, Ian Warren School of Computer Science, the University of Auckland, Scott Uk-Jin Lee Hanyang University
Not scheduled
Paper
Active Learning of Decomposable Systems
FormaliSE
Omar al Duhaiby Technische Universiteit Eindhoven (TU/e), Jan Friso Groote Technische Universiteit Eindhoven (TU/e)
Not scheduled
Paper
Lattice-Based Information Flow Control-by-Construction for Security-by-Design
FormaliSE
Tobias Runge TU Braunschweig, Alexander Knüppel TU Braunschweig, Thomas Thüm University of Ulm, Ina Schaefer TU Braunschweig
Not scheduled
Paper
Towards Formally Verified Key Management for Industrial Control Systems
FormaliSE
Tomas Kulik Aarhus University, Jalil Boudjadar Aarhus University, Diego F. Aranha Aarhus University
Not scheduled
Paper
HaiQ: Synthesis of Software Design Spaces with Structural and Probabilistic Guarantees
FormaliSE
Javier Camara University of York

Accepted Papers

Title
Active Learning of Decomposable Systems
FormaliSE
Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study
FormaliSE
HaiQ: Synthesis of Software Design Spaces with Structural and Probabilistic Guarantees
FormaliSE
Lattice-Based Information Flow Control-by-Construction for Security-by-Design
FormaliSE
Mind the gap: Robotic Mission Planning Meets Software Engineering
FormaliSE
Minimal Assumptions Refinement for Realizable Specifications
FormaliSE
Relational Test Tables: A Practical Specification Language for Evolution and Security
FormaliSE
Rule-based Word Equation Solving
FormaliSE
Security Analysis of a Quadruple-tank Water System via Statistical Model Checking
FormaliSE
Security Verification of Industrial Control Systems using Partial Model Checking
FormaliSE
Semantic-based Architecture Smell Analysis
FormaliSE
Towards Formally Verified Key Management for Industrial Control Systems
FormaliSE
UML consistency rules: a case study with open-source UML models
FormaliSE
Verification of Privacy-Enhanced Collaborations
FormaliSE

Call for Papers

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, CI/CD)
  • requirements formalization and formal specification;
  • model-based 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;

We invite you to submit:

  • Full research papers that must describe authors’ original research work and results.
  • 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.

Full and case study papers are limited to 10 pages, including all text, figures, tables, and appendices, plus up to 2 additional pages of references; research ideas papers are limited to 4 pages plus up to 1 additional page of references. All submissions must be in English and in PDF format. The page limit is strict, and it will not be possible to purchase additional pages at any point in the process (including after the paper is accepted).

Formatting instructions are available at https://www.acm.org/publications/proceedings-template for both LaTeX and Word users. LaTeX users must use the provided acmart.cls and ACM-Reference-Format.bst without modification, enable the conference format in the preamble of the document (i.e., \documentclass[sigconf,review]{acmart}), and use the ACM reference format for the bibliography (i.e., \bibliographystyle{ACM-Reference-Format}). The review option adds line numbers, thereby allowing referees to refer to specific lines in their comments.

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

Submissions to FormaliSE 2020 that meet the above requirements can be made via the submission site https://formalise2020.hotcrp.com/ by the submission deadline. 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.

All accepted publications are published as part of the ICSE 2020 Proceedings in the ACM and IEEE Digital Libraries. The official publication date of the conference proceedings is the date the proceedings are made available in the ACM Digital Library. The official publication date affects the deadline for any patent filings related to published work.

If a submission is accepted, at least one author of the paper is required to attend the conference and present the paper in person. If not, the paper will be removed from the proceedings.

Important dates:

  • Abstract submission: 16 January 2020
  • Paper submission: 23 January 2020
  • Notifications: 1 March 2020
  • Camera ready copies: 16 March 2020
  • FormaliSE conference: 13 July 2020

General Chairs

  • Stefania Gnesi, ISTI-CNR, Italy
  • Nico Plat, Thanos, The Netherlands

Program Chairs

  • Kyungmin Bae, POSTECH (Pohang University of Science and Technology), South Korea
  • Domenico Bianculli, University of Luxembourg, Luxembourg

We can be reached at oc@formalise.org. If you intend to submit a paper you are invited to inform us in advance.

The program committee consists of:

  • Ebru Aydin Gol, Middle East Technical University, Turkey
  • Toshiaki Aoki, JAIST, Japan
  • Maurice ter Beek, ISTI-CNR Pisa, Italy
  • Simon Bliudze, Inria Lille - Nord Europe, France
  • Einar Broch Johnsen, University of Oslo, Norway
  • Ana Cavalcanti, University of York, UK
  • Yunja Choi, Kyungpook National University, South Korea
  • Nancy Day, University of Waterloo, Canada
  • Marc Frappier, Université de Sherbrooke, Canada
  • Carlo A. Furia, USI (Università della Svizzera italiana), Switzerland
  • Osman Hasan, National University of Sciences & Technology, Pakistan
  • Marie-Christine Jakobs, TU Darmstadt, Germany
  • Eunsuk Kang, Carnegie Mellon University, USA
  • Axel Legay, UC Louvain, Belgium
  • Mieke Massink, ISTI-CNR Pisa, Italy
  • Claudio Menghi, University of Luxembourg, Luxembourg
  • Magnus O. Myreen, Chalmers University of Technology, Sweden
  • Kazuhiro Ogata, Japan Advanced Institute of Science and Technology, Japan
  • Peter Ölveczky, University of Oslo, Norway
  • Patrizio Pelliccione, University of L’Aquila, Italy and Chalmers | University of Gothenburg, Sweden
  • Rahul Purandare, IIIT-Delhi, India
  • Matteo Rossi, Politecnico di Milano, Italy
  • Gwen Salaün, Université Grenoble Alpes, France
  • Gerardo Schneider, University of Gothenburg, Sweden
  • Sibylle Schupp, Hamburg University of Technology, Germany
  • Jorge Sousa Pinto, University of Minho & INESC TEC, Portugal
  • Paola Spoletini, Kennesaw State University, USA
  • Meng Sun, Peking University, China
  • Stefano Tonetta, FBK, Italy
  • Michael Whalen, Amazon, Inc., USA

Questions? Use the FormaliSE contact form.