FormaliSE 2020

The 8th Conference on Formal Methods in Software Engineering, FormaliSE 2020, was organized as a one-day virtual event 13 July. All paper presentations were asynchronous, i.e. all authors recorded a video of their presentation and uploaded it to Youtube. The event was attended by roughly 73 researchers, including people from industry as well as academia in the area of Formal Verification from around the globe.

Proceedings

The proceedings of the conference were published as part of the ICSE 2020 Workshop Proceedings in the ACM and IEEE Digital Libraries.

Program

Session 1 (13 July 2020, 7:00 UTC (12AM in US (Pacific), 3AM in US (Eastern), 8AM in UK, 9AM in central Europe, 4PM South Korea, 7PM in New Zealand)).

Part 1: Invited talk by Shahar Maoz

Shahar Maoz is an Associate Professor at the School of Computer Science in Tel Aviv University, where he heads the Software Modeling Laboratory. Shahar has a BSc and MSc computer science degrees from Tel Aviv University, and a PhD from the Weizmann Institute. From 2010 to 2012 he was post-doc research fellow in RWTH Aachen University, Germany, with a postdoctoral fellowship from the Minerva Foundation. In 2015-2016 he spent a sabbatical at MIT CSAIL. Shahar's research interests are in software engineering, specifically in the use of models and formal methods for software evolution, model inference, testing, and synthesis. His work has been published in top software engineering and modeling conferences and journals. He is a recipient of an ERC Starting Grant for the development of synthesis technologies for reactive systems software engineers (project SYNTECH).

Title of the keynote: SYNTECH: Synthesis Technologies for Reactive Systems Software Engineers (presentation on YouTube)

Abstract: Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given declarative, temporal specification. Examples of these systems include the software controllers of robotic systems. Despite recent advancements on the theory and algorithms of reactive synthesis, e.g., efficient synthesis for the GR(1) fragment of linear temporal logic, many challenges remain in bringing reactive synthesis technologies to the hands of software engineers. The SYNTECH project is about bridging this gap. It addresses challenges that relate to the change from writing code to writing specifications, and the development of tools to support a specification-centric rather than a code-centric software development process. In this talk I will give an overview of the SYNTECH project’s results from the last five years. These include the Spectra specification language and Spectra Tools, a synthesizer and related analyses aiming at helping engineers write better specifications for synthesis. I will also present the application of Spectra to classic problems as well as to autonomous Lego robots and some example simulated systems, as developed by undergraduate computer science students in project classes we have taught. Finally, I will discuss new challenges and research opportunities.

The talk will cover results from papers in ESEC/FSE’15, ESEC/FSE’16, ESEC/FSE’17, ICSE’19, and FM'19. Joint work with Gal Amram, Elizabeth Firman, Aviv Kuvent, Or Pistiner, Jan O. Ringert, and Rafi Shalom. The project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH). For more information, see http://smlab.cs.tau.ac.il/syntech/.

 
Part 2: Q&A for questions and discussion of the pre-recorded paper presentations by authors (one hour) 

Session 2 (13 July 2020, 15:00 UTC (8AM in US (Pacific), 11AM in US (Eastern), 4PM in UK, 5PM in central Europe, 12AM (+1d) South Korea, 3AM (+1d) in New Zealand)).

Part 1: Invited talk by Corina Pasareanu

Corina Pasareanu is an Associate Research Professor with CyLab at Carnegie Mellon University, working at the Silicon Valley campus with NASA Ames Research Center. Her research interests include: model checking and automated testing, compositional verification, model-based development, probabilistic software analysis, and autonomy and Security. She is the recipient of several awards, including ASE Most Influential Paper Award (2018), ESEC/FSE Test of Time Award (2018), ISSTA Retrospective Impact Paper Award (2018), ACM Distinguished Scientist (2016), ACM Impact Paper Award (2010), ICSE 2010 Most Influential Paper Award (2010).

Title of the keynote: On the Probabilistic Analysis of Neural Networks (presentation on YouTube)

Abstract: Neural networks are powerful tools for automated decision-making, seeing increased application in safety-critical domains, such as autonomous driving. Due to their black-box nature and large scale, reasoning about their behavior is challenging. Statistical analysis is often used to infer probabilistic properties of a network, such as its robustness to noise and inaccurate inputs. While scalable, statistical methods can only provide probabilistic guarantees on the quality of their results and may underestimate the impact of low probability inputs leading to undesired behavior of the network. We investigate here the use of symbolic analysis and constraint solution space quantification to precisely quantify probabilistic properties in neural networks. We demonstrate the potential of the proposed technique in a case study involving the analysis of ACAS-Xu, a collision avoidance system for unmanned aircraft control.

 
Part 2: Q&A for questions and discussion of the pre-recorded paper presentations by authors (one hour)

 

Presentations on accepted papers available on YouTube (click here for abstracts of these papers):

Verification of Privacy-Enhanced Collaborations (presentation on YouTube)
S. Belluccini, R. De Nicola, M. Dumas, P. Pullonen, B. Re, F. Tiezzi

UML consistency rules: a case study with open-source UML models (presentation on YouTube)
D. Torre, Y. Labiche, M. Genero, M. Elaasar, C. Menghi 

Towards Formally Verified Key Management for Industrial Control Systems (presentation on YouTube)
T. Kulik, J. Boudjadar, D. Aranha

Rule-based Word Equation Solving (presentation on YouTube)
J. Day, M. Kulczynski, F. Manea, D. Nowotka, D. Poulsen 

Minimal Assumptions Refinement for Realizable Specifications (presentation on YouTube)
D. Cavezza, D. Alrajeh, A. György

Security Verification of Industrial Control Systems using Partial Model Checking (presentation on YouTube)
T. Kulik, J. Boudjadar, P. Tran-Jørgensen 

Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study  (presentation on YouTube)
S. Foster, Y. Nemouchi, C. O'Halloran, K. Stephenson, N. Tudor 

Active Learning of Decomposable Systems (presentation on YouTube)
O. al Duhaiby, J. Groote 

Mind the gap: Robotic Mission Planning Meets Software Engineering (presentation on YouTube)
M. Askarpour, C. Menghi, G. Belli, M. Bersani, P. Pelliccione

HaiQ: Synthesis of Software Design Spaces with Structural and Probabilistic Guarantees (presentation on YouTube)
J. Camara 

Security Analysis of a Quadruple-tank Water System via Statistical Model Checking  (presentation on YouTube)
Munteanu, M. Pasqua, M. Merro 

Semantic-based Architecture Smell (presentation on YouTube)
N. Chondamrongkul, J. Sun, I. Warren, S. Lee 

Lattice-Based Information Flow Control-by-Construction for Security-by-Design  (presentation on YouTube)
T. Runge, A. Knüppel, T. Thüm, I. Schaefer 

Relational Test Tables: A Practical Specification Language for Evolution and Security (presentation on YouTube)
Weigl, M. Ulbrich, S. Cha, B. Beckert, B. Vogel-Heuser

 

PC Chairs

PC Chairs for FormaliSE 2020 were:

 

Social Media Chair:

 

Programme Committee

  • 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
  • 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
  • Ebru Aydin Gol, Middle East Technical University, Turkey
  • Osman Hasan, National University of Sciences & Technology , Pakistan
  • Marie-Christine Jakobs, TU Darmstadt, Germany
  • Einar Broch Johnsen, University of Oslo, Norway
  • 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

 

Organizing Committee

Organizing Committee members for FormaliSE 2020: