Program

Programme 

Keynotes

    • Title: Digital Twins: An Emerging Paradigm for Model-Centric Engineering

Speaker: Einar Broch Johnsen, University of Oslo, Norway
Einar image
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.
Homepage
https://ebjohnsen.org

 

    • Title: Formal methods for dealing with traffic rules in autonomous driving

Speaker: Jana Tumova, KTH Royal Institute of Technology, Sweden

Jana Image
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.
Homepage
https://sites.google.com/view/janatumova

    • Title: Integrating Usability into Language and Type System Design 

SpeakerJonathan 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.
Homepage
https://www.cs.cmu.edu/~aldrich/

 

 

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

    1. Generating Counterexamples in the form of Unit Tests from Hoare-style Verification Attempts
      (Amirfarhad Nilizadeh, Marlon Calvo, Gary T. Leavens and David Cok)
    2. 5-minute teaser: Property-Driven Testing of Black-Box Functions
      (Arnab Sharma, Vitalik Melnikov, Eyke Hüllermeier and Heike Wehrheim)
    3. 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

    1. Towards Automated Input Generation for Sketching Alloy Models
      (Ana Jovanovic and Allison Sullivan)
    2. Automating Cryptographic Protocol Language Generation from Structured Specifications
      (Roberto Metere and Luca Arnaboldi)
    3. 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

    1. Towards Automated Input Generation for Sketching Alloy Models
      (Ana Jovanovic and Allison Sullivan)
    2. Automating Cryptographic Protocol Language Generation from Structured Specifications
      (Roberto Metere and Luca Arnaboldi)
    3. Counterexample-Guided Inductive Repair of Reactive Contracts
      (Soha Hussein, Sanjai Rayadurgam, Stephen McCamant, Vaibhav Sharma and Mats Heimdahl)
    4. 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

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

 

Closing & Outlook