FormaliSE 2022

Proceedings

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

Title: Digital Twins: An Emerging Paradigm for Model-Centric Engineering
Speaker: Einar Broch Johnsen, University of Oslo, Norway
Abstract. Digital twins are emerging as an engineering paradigm to build software centred around models of physical objects or processes. In engineering, the use of digital twins profoundly changes the entire product lifecycle management, from design to manufacturing and operations, because the digital twins adapt in response to the evolution of their physical counterpart. The purpose of the digital twin is to understand, predict and act on the behaviour of these physical systems. Digital twins can evolve continuously based on real-time streams of observations from the physical system combined with artefacts developed during the design stage. In this talk, we move from the engineering of digital twins to the science of digital twins. We consider basic concepts of digital twins, present some examples of how we can work with them in research, and discuss emerging research challenges at the intersection of formal methods and software engineering.
Bio. Einar Broch Johnsen is a professor and the head of the Formal Methods group at the Department of Informatics, University of Oslo. His research interests include programming models and methodology; program specification and modeling; and the theory and application of formal methods. He is active in formal methods for distributed and concurrent systems, including object-oriented and concurrent languages, manycore computing, cloud computing, and digital twins. He is one of the main developers of the ABS modeling language.

Title: Formal methods for dealing with traffic rules in autonomous driving
Speaker: Jana Tumova, KTH Royal Institute of Technology, Sweden
Abstract. Motion planning for autonomous vehicles has to be able to cope with various complex requirements from following the rules of the road, avoiding (dynamic) obstacles, dealing with unusual circumstances, as well driving in a socially compliant way. In this talk, we present an approach combining formal methods with traditional motion planning and control algorithms to attack this challenge. We discuss the use of Linear Temporal Logic (LTL) and Signal Temporal Logic (STL) to express traffic rules and driving styles. We present quantitative semantics to recognize the maximally compliant motion plans and algorithms to compute those. In particular, we focus on risk-aware autonomous driving under uncertainty: We suggest a risk measure that captures the probability of violating the specification and determines the average expected severity of violation. Using highway scenarios of the US101 dataset and Responsibility-Sensitive Safety (RSS) model as an example specification, we demonstrate that by incorporating the risk measure into a trajectory planner, we enable autonomous vehicles to plan minimal-risk trajectories and to quantify trade-offs between risk and progress in traffic scenarios.
Bio. Jana Tumova is an associate professor at the Division of Robotics, Perception and Learning, School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology. She received PhD in computer science from Masaryk University and was awarded ACCESS postdoctoral fellowship at KTH in 2013. She was also a visiting researcher at MIT, Boston University, and Singapore-MIT Alliance for Research and Technology. Her research interests include formal methods applied in decision making, motion planning, and control of autonomous systems. Among other awards, she is a recipient of a Swedish Research Council Starting Grant, RSS Early Career Award and a WASP Expeditions project focusing on design of socially acceptable and correct-by-design autonomous systems.

Title: Integrating Usability into Language and Type System Design
Speaker: Jonathan Aldrich, Carnegie Mellon University, USA
Abstract. Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, we propose gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. I’ll describe a system that can verify first-order specifications of programs that manipulate recursive, mutable data structures on the heap, demonstrate a prototype tool, and share some initial empirical results. Our approach addresses several technical challenges, such as semantically connecting iso- and equi-recursive interpretations of abstract predicates, and supporting gradual verification of heap ownership. This work thus lays the foundation for future tools that work on realistic programs and support verification within an engineering process in which cost-benefit tradeoffs can be made.
Bio. Jonathan Aldrich is a Professor of Computer Science at Carnegie Mellon University. He teaches courses in programming languages, software engineering, object-oriented design, and program analysis for quality and security. Prof. Aldrich directed CMU's Software Engineering Ph.D. program from 2013-2019. Dr. Aldrich’s research centers on programming languages and type systems that are deeply informed by software engineering considerations. His research contributions include modular and gradual verification of functional properties, typestate, and architectural structure, as well as the design of languages and type systems for usability. His notable awards include an NSF CAREER award (2006), the Dahl-Nygaard Junior Prize (2007), the DARPA Computer Science Study Group, and an ICSE most influential paper award (2012). He served as general chair (2015), program chair (2017), and steering committee chair (2017-2019) of SPLASH and OOPSLA. Aldrich holds a bachelor's degree in Computer Science from Caltech and a Ph.D. from the University of Washington.

Programme

Virtual Day 1 (18 May 2022)

15:00-16:00 CEST / 09:00-10:00 EDT - Keynote

Formal methods for dealing with traffic rules in autonomous driving
(Jana Tumova, KTH Royal Institute of Technology, Sweden)

- Break -

16:30-17:45 CEST / 10:30-11:45 EDT

Formal Modeling and Verification of Multi-Robot Interactive Scenarios in Service Settings
(Livia Lestingi, Giorgio Romeo, Cristian Sbrolli, Pasquale Scarmozzino, Marcello M. Bersani and Matteo Rossi)

5-minute teaser: Counterexample-Guided Inductive Repair of Reactive Contracts
(Soha Hussein, Sanjai Rayadurgam, Stephen McCamant, Vaibhav Sharma and Mats Heimdahl)

Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers
(Sophie Lathouwers and Marieke Huisman)

- Break -

18:00-19:30 CEST / 12:00-13:30 EDT

Computing Program Functions
(Hessamaldin Mohammadi, Wided Ghardallou, Richard Linger and Ali Mili)

C for Yourself: Comparison of Front-End Techniques for Formal Verification
(Levente Bajczi, Zsófia Ádám and Vince Molnár)

Test Suite Generation for Boolean Conditions with Equivalence Class Partitioning
(Sylvain Hallé)

Virtual Day 2 (19 May 2022)

15:00-16:00 CEST / 09:00-10:00 EDT - Keynote

Digital Twins: An Emerging Paradigm for Model-Centric Engineering
(Einar Broch Johnsen, University of Oslo, Norway)

- Break -

16:30-17:45 CEST / 10:30-11:45 EDT

Generating Counterexamples in the form of Unit Tests from Hoare-style Verification Attempts
(Amirfarhad Nilizadeh, Marlon Calvo, Gary T. Leavens and David Cok)

5-minute teaser: Property-Driven Testing of Black-Box Functions
(Arnab Sharma, Vitalik Melnikov, Eyke Hüllermeier and Heike Wehrheim)

Counting Bugs in Behavioural Models using Counterexample Analysis
(Irman Faqrizal and Gwen Salaün)

- Break -

18:00-19:30 CEST / 12:00-13:30 EDT

Towards Automated Input Generation for Sketching Alloy Models
(Ana Jovanovic and Allison Sullivan)

Automating Cryptographic Protocol Language Generation from Structured Specifications
(Roberto Metere and Luca Arnaboldi)

Automatic Loop Invariant Generation for Data Dependence Analysis
(Asmae Heydari Tabar, Richard Bubel and Reiner Hähnle)

In-Person Day (22 May 2022)

Location: Room GHC 6115 at Carnegie Mellon University, Pittsburgh

10:00-10:45 EDT:

Check-in (with light breakfast)

10:45-12:00 EDT:

Opening
Keynote: Integrating Usability into Language and Type System Design
(Jonathan Aldrich, Carnegie Mellon University, USA)

12:00-14:00 EDT: 

Lunch (Carnegie Cafe)

14:00-16:00 EDT

Towards Automated Input Generation for Sketching Alloy Models
(Ana Jovanovic and Allison Sullivan)

Automating Cryptographic Protocol Language Generation from Structured Specifications
(Roberto Metere and Luca Arnaboldi)

Counterexample-Guided Inductive Repair of Reactive Contracts
(Soha Hussein, Sanjai Rayadurgam, Stephen McCamant, Vaibhav Sharma and Mats Heimdahl)

Property-Driven Testing of Black-Box Functions
(Arnab Sharma, Vitalik Melnikov, Eyke Hüllermeier and Heike Wehrheim)

16:00-16:30 EDT: Coffee break

16:30-17:30 EDT

Invited Tutorial: Formally Validating Model-Based Safety Assurance Cases
(Torin Viger, University of Toronto, Canada)

Closing & Outlook

Organization

General Chairs

- Stefania Gnesi (Istituto di Scienza e Tecnologie dell'Informazione, Italy)
- Nico Plat (Thanos, The Netherlands)

Program Chairs

- Ina Schaefer (TU Braunschweig, Germany)
- Arnd Hartmanns (University of Twente, The Netherlands)

Artifact Evaluation Chair

- Carlos E. Budde (Università degli Studi di Trento, Italy)

Social Media Chair

- Claudio Menghi (McMaster University, Canada)

Program committee

- Toshiaki Aoki (Japan Advanced Institute of Science and Technology, Japan)
- Kyungmin Bae (Pohang University of Science and Technology, South Korea)
- Simon Bliudze (INRIA Lille, France)
- Rabéa Ameur Boulifa (Télécom Paris, France)
- Christiano Braga (Universidade Federal Fluminense, Brazil)
- Ana Cavalcanti (University of York, UK)
- Nancy Day (University of Waterloo, Canada)
- Carlo Furia (Università della Svizzera italiana, Switzerland)
- Ebru Aydin Gol (Middle East Technical University, Turkey)
- Roberta Gori (Università di Pisa, Italy)
- Laura R. Humphrey (Air Force Research Laboratory, USA)
- Marie-Christine Jakobs (Technische Universität Darmstadt, Germany)
- Sebastian Junges (Radboud Universiteit, The Netherlands)
- Wanwei Liu (National University of Defense Technology, China)
- Malte Lochau (Universität Siegen, Germany)
- Antónia Lopes (Universidade de Lisboa, Portugal)
- Mieke Massink (Istituto di Scienza e Tecnologie dell'Informazione, Italy)
- Anastasia Mavridou (NASA Ames Research Center, USA)
- Hernán Melgratti (Universidad de Buenos Aires, Argentina)
- Alex Potanin (Victoria University of Wellington, New Zealand)
- Gwen Salaün (Université Grenoble Alpes, France)
- Sean Sedwards (University of Waterloo, Canada)
- Laura Semini (Università di Pisa, Italy)
- Silvia Lizeth Tapia Tarifa (Universitetet i Oslo, Norway)
- Maurice ter Beek (Istituto di Scienza e Tecnologie dell'Informazione, Italy)
- Andrea Turrini (Institute of Software, Chinese Academy of Sciences, China)
- Marcel Verhoef (European Space Agency, The Netherlands)
- Heike Wehrheim (Universität Paderborn, Germany)