STAF 2023
Tue 18 - Fri 21 July 2023 Leicester, United Kingdom

We are excited to announce five invited speakers from across the STAF’23 conferences (ECMFA, ICGT, and TAP):

TAP’23: Kim G. Larsen, Aalborg University (Denmark)

Symbolic, Statistical and Randomized Engines in UPPAAL

Tuesday 11am, Oak

UPPAAL provides a tool-suite supporting model checking, performance analysis, testing, synthesis and learning for real-time systems. Based on the underlying modeling formalism of timed automata, significant effort has been put into development and implementation of efficient datastructures and algorithmic methods. By now these methods have resulted in a variety of symbolic, statistical and randomized engines.

In the talk I will present the three algorithmic methods and highlight their particular benefits individually and in combinations. This include: 1) Randomized methods are useful in early phases of development for fast discovery leaving the use of expensive symbolic verification to the end of development. 2) Combining randomized and statistical methods we have proposed a new falsification testing methodology that is aware of expected system usage and underlying risks associated with different faulty behaviors, allowing for a ranking of counterexamples based on their expected impact. 3) UPPAAL Stratego combines symbolic and statistical (learning) methods for constructing safe and near-optimal control strategies.

We shall also report on current effort made towards a hierarchical modelling formalism, where first prototypes are being obtained using model transformations to the existing non-hierarchical formalism.

Finally during the talk we will provide on-line demo of the new release UPPAAL 5.0.

ICGT’23: Dan Ghica, Huawei Research and University of Birmingham (UK)

Syntactic trinitarianism: terms, graphs, diagrams

Wednesday 9am, Oak

The concept of ‘syntax’ is commonly understood as the structure hidden in linear sequences of tokens, which in language and logic we commonly call ‘terms’. However, for the purpose of analysis and transformation, compilers use more efficient data structures to represent syntax, namely graphs. The gap between the linear (term) and graph syntax is elegantly bridged by a third formalism, namely that of string diagrams, a planar representation of terms in the categorical representation of syntax. In this tutorial talk I will show how the interplay of terms, graphs, and diagrams can help specify and implement complex analyses and transformations in compilers for higher-order programming languages, such as type inference, automatic differentiation, or closure conversion. This methodology is at the foundation of a new industrial-strength compiler being implemented currently at Huawei.

Most of the material I will discuss is based on the recent tutorial paper “Hierarchical string diagrams and applications” jointly with Fabio Zanasi (https://arxiv.org/abs/2305.18945).

TAP’23: Mattias Ulbrich, Karlsruhe Institute of Technology (Germany)

KeY: A Verification Platform For Java

Wednesday 1:30pm, Willow

In recent years and decades, the research community has unleashed a diverse variety of approaches to formally assess and establish the correctness of programs on the source code level. It is still an active research area how the results of different verification techniques can be brought together profitably.

In this talk, I will present how the verification ecosystem surrounding the KeY tool allows one to combine a number of successful approaches. At its core, KeY is a deductive verification engine for the formal analysis of Java programs annotated with formal specifications written in the Java Modeling Language. It employs a dynamic logic calculus for Java driven by symbolic execution. We will learn about the working principles of this verification method and see how it was used to prove (or disprove) the correctness of relevant real-world Java components, for instance from the JDK.

In addition, I will present the Karlsruhe Java Verification Suite (KaJaVe), where we enriched the KeY prover infrastructure by a number of approaches that leverage other verification principles such that they can be used in combination with the deductive verifier.

ICGT’23: Mohammad Abdulaziz, King’s College London (UK)

Formal Mathematics: Matching Algorithms as a Case Study

Thursday 1:30pm, Willow

A formal proof is a proof within an axiomatic system, where proof steps are either applications of axioms or applications of formally proven statements. Formal proofs have a long history within mathematics, starting with Euclid’s element’s which had an axiomatic system for geometrical reasoning. The main motivation of constructing a formal proof is obtaining unambiguous detailed proofs that can be mechanically checked. The advent of computer-based tools for formal proof, such as automatic and interactive theorem provers, made it feasible to produce formal versions of proofs that would otherwise be impossible.

A matching in an undirected graph is a subset of the edges of the graph s.t. no two edges are incident on the same vertex. In addition to the rich mathematical structure exhibited by matchings, algorithms to compute matchings have many applications, ranging from matching kidney donors and recipients to the allocation of advertisers to users of search engines.

In this talk, after giving an overview of the state-of-the-art, I will discuss my work on applying formal proof technology to matching theory, discussing some interesting findings and the even more interesting open questions.

Biography. Mohammad Abdulaziz is a lecturer (equiv. to assistant professor) and member of the Reasoning and Planning Group at King’s College London. Before that, he was a post-doc in the Chair for Logic and Verification at Technische Universität München. His main research is in the area of formal mathematics, with a special focus on formalising theoretical CS, and the formal verification of algorithms and software.

ECMFA’23: Andrzej Wąsowski, IT University of Copenhagen (Denmark)

How I lost my faith (in language technology research)? There and back again.

Friday 9am, Oak

Modeling and language engineering have hardly ever been as successful as today. Whatever software domain you zoom into, you will find plenty external and internal modeling languages. Everybody is doing (multi-)modeling all the time. At the same time modeling has never been as invisible as it is today. Modeling is not a buzzword. Being a modeling-expert means not much, when everybody is a modeling expert.

In this talk, I will zoom in into two groups of modeling languages: reactive programming languages including behavior trees and state machines (as used in robotics) and probabilistic programming languages (as used in data science). While looking at these examples closely, I want to answer three questions: Concretely how and by whom are these modeling languages engineered? Why and how should people be taught language engineering in 2023? And, finally, how can one be a modeling researcher in 2023?

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

Tue 18 Jul

Displayed time zone: London change

10:30 - 11:00
Morning CoffeeSocial at The Bar
10:30
30m
Coffee break
Coffee Break
Social

11:00 - 12:30
STAF Keynote / TAP Session 1Keynotes / TAP / ECMFA / ICGT Research Papers at Oak
Chair(s): Cristina Seceleanu Mälardalen University

Remote Participants: Zoom Link, YouTube Livestream

11:00
15m
Day opening
TAP Conference Opening
TAP
Virgile Prevosto CEA Tech List, Cristina Seceleanu Mälardalen University
11:15
75m
Keynote
Symbolic, Statistical and Randomized Engines in UPPAAL
Keynotes
Kim Larsen Aalborg University
12:30 - 13:30
12:30
60m
Lunch
Lunch
Social

13:30 - 15:00
TAP Session 2: Low-level code verificationTAP at Oak
Chair(s): Julien Signoles Université Paris-Saclay, CEA, List

Remote Participants: Zoom Link

13:30
30m
Talk
BIRD: A Binary Intermediate Representation for formally verified Decompilation of x86-64 binaries
TAP
P: Daniel Engel Open University Of The Netherlands, Freek Verbeek Open University of the Netherlands, The Netherlands, Binoy Ravindran Virginia Tech
DOI Pre-print File Attached
14:00
30m
Talk
Low-level Reachability Analysis based on Formal Logic
TAP
P: Nico Naus Virginia Tech, Freek Verbeek Open University of the Netherlands, The Netherlands, Marc Schoolderman Radboud University Nijmegen, Binoy Ravindran Virginia Tech
DOI Pre-print
14:30
30m
Talk
Testing a Formally Verified Compiler
TAP
P: David Monniaux CNRS/VERIMAG, Léo Gourdin Université Grenoble Alpes, Verimag, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Olivier Lebeltel Université Grenoble Alpes, CNRS, Verimag
DOI Pre-print
15:30 - 16:30
TAP Session 3: Formal ModelsTAP at Oak
Chair(s): Catherine Dubois ENSIIE Paris-Evry

Remote Participants: Zoom Link

15:30
30m
Talk
Certified Logic-Based Explainable AI -- The Case of Monotonic Classifiers
TAP
P: Aurélie Hurault IRIT - ENSEEIHT, Joao Marques-Silva IRIT, CNRS, Toulouse
DOI File Attached
16:00
30m
Talk
Context Specification Language for Formal Verification of Consent Properties on Models and Code
TAP
P: Myriam Clouet Université Paris-Saclay, CEA, List, Thibaud Antignac CNIL (Commission nationale de l’informatique et des libertés), Mathilde Arnaud Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List
DOI File Attached

Wed 19 Jul

Displayed time zone: London change

09:00 - 10:15
STAF Keynote / ICGT Session 1Keynotes / TAP / ECMFA / ICGT Research Papers at Oak
Chair(s): Maribel Fernandez King's College London

Remote Participants: Zoom Link, YouTube Livestream

09:00
15m
Day opening
ICGT Conference Opening
ICGT Research Papers
Maribel Fernandez King's College London, Chris Poskitt Singapore Management University
File Attached
09:15
60m
Keynote
Syntactic trinitarianism: terms, graphs, diagrams
Keynotes
Dan Ghica Huawei Research and University of Birmingham
Pre-print
10:30 - 11:00
Morning CoffeeSocial at The Bar
10:30
30m
Coffee break
Coffee Break
Social

11:00 - 12:30
ICGT Session 2: Specification and VerificationICGT Research Papers at Oak
Chair(s): Arend Rensink University of Twente, The Netherlands

Remote Participants: Zoom Link, YouTube Livestream

11:00
30m
Talk
Specification and Verification of a Linear-time Temporal Logic for Graph Transformation
ICGT Research Papers
Fabio Gadducci University of Pisa, P: Andrea Laretto Tallinn University of Technology, Davide Trotta University of Pisa
DOI Pre-print File Attached
11:30
30m
Talk
Mechanised DPO Theory: Uniqueness of Derivations and Church-Rosser TheoremICGT Best Theory Paper
ICGT Research Papers
P: Robert Söldner University of York, Detlef Plump University of York
DOI
12:00
30m
Talk
Formalisation, Abstraction and Refinement of Bond Graphs
ICGT Research Papers
P: Richard Banach University of Manchester, John Baugh North Carolina State University
DOI
11:15 - 12:45
TAP Session 4: Model-based test generationTAP at Willow
Chair(s): Nico Naus Virginia Tech

Remote Participants: Zoom Link

11:15
30m
Talk
Symbolic Observation Graph-Based Generation of Test Paths
TAP
P: Kais Klai Universit Paris 13, Mohamed Taha Bennani Universty of Tunis El Manar, Jaime Arias CNRS; LIPN; Université Sorbonne Paris Nord, Jörg Desel Fernuniversität in Hagen, Hanen Ochi EFREI
DOI File Attached
11:45
30m
Talk
Testing Languages with a Languages-as-databases ApproachTAP Best Paper
TAP
P: Matteo Cimini University of Massachusetts Lowell
DOI
12:15
30m
Talk
Proving Properties of Operation Contracts with Test Scenarios
TAP
P: Martin Gogolla Database Systems Group, University of Bremen, Lars Hamann HAW Hamburg
DOI
13:30 - 15:00
ICGT Session 3: TheoryICGT Research Papers at Oak
Chair(s): Nicolas Behr CNRS, Université Paris Cité, IRIF

Remote Participants: Zoom Link, YouTube Livestream

13:30
30m
Talk
A Monoidal View on Fixpoint Checks
ICGT Research Papers
Paolo Baldan University of Padova, P: Richard Eggert University of Duisburg-Essen, Barbara König University of Duisburg-Essen, Timo Matt University Duisburg-Essen, Tommaso Padoan University of Padova
DOI Pre-print
14:00
30m
Talk
Fuzzy Presheaves are Quasitoposes
ICGT Research Papers
P: Aloïs Rosset Vrije Universiteit Amsterdam, Roy Overbeek Vrije Universiteit Amsterdam, Jörg Endrullis Vrije Universiteit Amsterdam
DOI File Attached
14:30
30m
Talk
Moving a Derivation Along a Derivation Preserves the Spine
ICGT Research Papers
P: Hans-Jörg Kreowski University of Bremen, Sabine Kuske University of Bremen, Aaron Lye University of Bremen, Aljoscha Windhorst University of Bremen
DOI
13:45 - 15:15
TAP Session 5: KeynoteKeynotes at Willow
Chair(s): Virgile Prevosto CEA Tech List

Remote Participants: Zoom Link

13:45
90m
Keynote
KeY: A Verification Platform For Java
Keynotes
15:30 - 17:00
ICGT Session 4: Graph Transformation PropertiesICGT Research Papers / ICGT Journal-First at Oak
Chair(s): Russ Harmer CNRS

Remote Participants: Zoom Link, YouTube Livestream

15:30
30m
Talk
Finding the Right Way to Rome: Effect-oriented Graph Transformation
ICGT Research Papers
P: Jens Kosiol Universität Kassel, Daniel Strüber Chalmers | University of Gothenburg / Radboud University, Gabriele Taentzer Philipps-Universität Marburg, Steffen Zschaler King's College London
DOI Pre-print File Attached
16:00
30m
Talk
Termination of Graph Transformation Systems using Weighted Subgraph CountingNominated for Best Paper
ICGT Research Papers
P: Roy Overbeek Vrije Universiteit Amsterdam, Jörg Endrullis Vrije Universiteit Amsterdam
DOI Pre-print File Attached
16:30
30m
Talk
Extending single- to multi-variant model transformations by trace-based propagation of variability annotations
ICGT Journal-First
P: Bernhard Westfechtel University of Bayreuth, Sandra Greiner University of Bern, Switzerland
DOI File Attached
15:45 - 16:45
TAP Session 6: Abstraction and RefinementTAP at Willow
Chair(s): Matteo Cimini University of Massachusetts Lowell

Remote Participants: Zoom Link

15:45
30m
Talk
Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion CheckingTAP Best Paper
TAP
P: Thibaut Benjamin Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List
DOI
16:15
30m
Talk
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
TAP
P: Megan Strauss Carnegie Mellon University, Stefan Mitsch Carnegie Mellon University, USA
DOI

Thu 20 Jul

Displayed time zone: London change

09:00 - 10:30
ICGT Session 5: Blue Skies & Journal-FirstICGT Research Papers / ICGT Journal-First at Willow
Chair(s): Detlef Plump University of York

Remote Participants: Zoom Link, YouTube Livestream

09:00
30m
Talk
A living monograph for graph transformation
ICGT Research Papers
Nicolas Behr CNRS, Université Paris Cité, IRIF, P: Russ Harmer CNRS
DOI File Attached
09:30
30m
Talk
Graph Rewriting for Graph Neural NetworksNominated for Best Paper
ICGT Research Papers
Adam Machowczyk University of Leicester, P: Reiko Heckel University of Leicester
DOI File Attached
10:00
30m
Talk
Compositionality of Rewriting Rules with Conditions
ICGT Journal-First
P: Nicolas Behr CNRS, Université Paris Cité, IRIF, Jean Krivine CNRS
DOI Media Attached
09:30 - 10:45
ECMFA Session 1: Tools and ModularityECMFA at Oak
Chair(s): Jesús Sánchez Cuadrado Universidad de Murcia

Remote Participants: Zoom Link

09:30
15m
Day opening
ECMFA Conference Opening
ECMFA
P: Jesús Sánchez Cuadrado Universidad de Murcia, Steffen Zschaler King's College London
09:45
30m
Talk
Concern-Oriented Use Cases
ECMFA
P: Ryan Languay McGill University, Nika Prairie McGill University, Jörg Kienzle McGill University, Canada
DOI File Attached
10:15
30m
Talk
The OSATE Slicer: Graph-Based Reachability for Architectural Models
ECMFA
P: Sam Procter Carnegie Mellon Software Engineering Institute
DOI Pre-print File Attached
11:00 - 12:30
ICGT Session 6: ApplicationsICGT Research Papers at Willow
Chair(s): Kazunori Ueda Waseda University

Remote Participants: Zoom Link, YouTube Livestream

11:00
30m
Talk
A Rule-Based Procedure for Graph Query Solving
ICGT Research Papers
Dominique Duval Université Grenoble Alpes, P: Rachid Echahed University of Grenoble - CNRS, Frederic Prost Université Grenoble Alpes
DOI
11:30
30m
Talk
Formalization and analysis of BPMN using graph transformation systemsICGT Best Applications Paper
ICGT Research Papers
P: Tim Kräuter Western Norway University of Applied Sciences, Adrian Rutle Western Norway University of Applied Sciences, Harald König University of Applied Sciences, FHDW Hannover and Western Norway University of Applied Sciences, Yngve Lamo Western Norway University of Applied Sciences
DOI Pre-print File Attached
12:00
30m
Talk
Dominant Eigenvalue-Eigenvector Pair Estimation via Graph Infection
ICGT Research Papers
P: Kaiyuan Yang University of Zurich, Li Xia National University of Singapore, Y.C. Tay National University of Singapore
DOI Pre-print
11:15 - 12:45
ECMFA Session 2: Industrial and ApplicationsECMFA at Oak
Chair(s): Juan de Lara Autonomous University of Madrid

Remote Participants: Zoom Link

11:15
30m
Talk
A model-based framework for IoT systems in wastewater treatment plants
ECMFA
P: Iván Alfonso Internet Interdisciplinary Institute, Universitat Oberta de Catalunya, Abel Gómez Universitat Oberta de Catalunya, Silvia Doñate Depuración de Aguas del Mediterráneo, kelly Garces Pernett Universidad de los Andes , Bogotá, Colombia, Harold Castro Department of Systems and Computing Engineering, Universidad de los Andes, Colombia, Jordi Cabot Luxembourg Institute of Science and Technology
DOI
11:45
30m
Talk
Bridging the Gap between SysML and OPC UA Information Models for Industry 4.0
ECMFA
P: Fadwa Rekik Softeam, Saadia Dhouib CEA LIST, Quang-Duy Nguyen Université Paris-Saclay, CEA, List
DOI File Attached
12:15
30m
Talk
Simulink bus usage in practice: an empirical study
ECMFA
P: Tiago Amorim University of Cologne, Alexander Boll University of Bern, Ferry Bachmann , Timo Kehrer University of Bern, Andreas Vogelsang University of Cologne, Hartmut Pohlheim
DOI Pre-print
13:30 - 15:00
ICGT Session 7: Keynote & Journal-FirstICGT Journal-First / Keynotes at Willow
Chair(s): Chris Poskitt Singapore Management University

Remote Participants: Zoom Link, YouTube Livestream

13:30
60m
Keynote
Formal Mathematics: Matching Algorithms as a Case Study
Keynotes
Mohammad Abdulaziz Technische Universität München
File Attached
14:30
30m
Talk
Fast Rule-Based Graph Programs
ICGT Journal-First
DOI
13:45 - 15:15
ECMFA Session 3: Domain-Specific LanguagesECMFA at Oak
Chair(s): Antonio Vallecillo University of Málaga, Spain

Remote Participants: Zoom Link

13:45
30m
Talk
Model-Driven Engineering for Augmented Reality
ECMFA
Rubén Campos-López Universidad Autónoma de Madrid, Esther Guerra Universidad Autónoma de Madrid, P: Juan de Lara Autonomous University of Madrid, Alessandro Colantoni Johannes Kepler University Linz, Antonio Garmendia Universidad Autónoma de Madrid
DOI Pre-print Media Attached
14:15
30m
Talk
Protocol-Based Interactive Debugging for Domain-Specific LanguagesNominated for Best Paper
ECMFA
P: Josselin Enet Nantes Université, Erwan Bousse Nantes Université, Massimo Tisi IMT Atlantique, LS2N (UMR CNRS 6004), Gerson Sunyé Nantes University
DOI
14:45
30m
Talk
Streamlining the Development of Hybrid Graphical-Textual Model Editors for Domain-Specific LanguagesNominated for Best Paper
ECMFA
P: Ionut Predoaia University of York, Dimitris Kolovos University of York, Matthias Lenk NetApp, Antonio Garcia-Dominguez University of York
DOI
15:30 - 17:15
ICGT Session 8: Tools & ApplicationsICGT Research Papers at Willow
Chair(s): Rachid Echahed University of Grenoble - CNRS

Remote Participants: Zoom Link, YouTube Livestream

15:30
30m
Talk
Implementing the λGT Language: A Functional Language with Graphs as First-Class Data
ICGT Research Papers
P: Jin Sano Waseda University, Kazunori Ueda Waseda University
DOI File Attached
16:00
30m
Talk
Computing k-Bisimulations for Large Graphs: A Comparison and Efficiency Analysis
ICGT Research Papers
Jannik Rau Ulm University, P: David Richerby University of Essex, Ansgar Scherp Ulm University
DOI Pre-print
16:30
30m
Talk
Advanced Consistency Restoration with Higher-Order Short-Cut Rules
ICGT Research Papers
P: Lars Fritsche TU Darmstadt, Germany, Jens Kosiol Universität Kassel, Adrian Möller TU Darmstadt, Germany, Andy Schürr TU Darmstadt, Germany
DOI
17:00
15m
Day closing
ICGT Conference Closing
ICGT Research Papers
Maribel Fernandez King's College London, Reiko Heckel University of Leicester, Chris Poskitt Singapore Management University
15:45 - 17:15
ECMFA Session 4: Model Differencing and MergingECMFA at Oak
Chair(s): Jörg Kienzle McGill University, Canada

Remote Participants: Zoom Link

15:45
30m
Talk
CDMerge: Semantically Sound Merging of Class Diagrams for Software Component Integration
ECMFA
Achim Lindt RWTH Aachen University, Chair of Software Engineering, Bernhard Rumpe RWTH Aachen University, P: Max Stachon RWTH Aachen University, Sebastian Stüber RWTH Aachen University, Chair of Software Engineering
DOI File Attached
16:15
30m
Talk
On Implementing Open World Semantic Differencing for Class Diagrams
ECMFA
Jan Oliver Ringert Bauhaus-University Weimar, Bernhard Rumpe RWTH Aachen University, P: Max Stachon RWTH Aachen University
DOI File Attached
16:45
30m
Talk
Evaluating Model Differencing for the Consistency Preservation of State-based ViewsECMFA Best Paper
ECMFA
Jan Willem Wittler Karlsruhe Institute of Technology, P: Timur Sağlam Karlsruhe Institute of Technology (KIT), Thomas Kühn Martin-Luther-University Halle-Wittenberg
DOI Media Attached File Attached

Fri 21 Jul

Displayed time zone: London change

09:00 - 10:30
STAF Keynote / ECMFA Session 5Keynotes / TAP / ECMFA / ICGT Research Papers at Oak
Chair(s): Steffen Zschaler King's College London

Remote Participants: Zoom Link, YouTube Livestream

09:00
90m
Keynote
How I lost my faith (in language technology research)? There and back again.
Keynotes
Andrzej Wąsowski IT University of Copenhagen, Denmark
10:30 - 11:00
Morning CoffeeSocial at The Bar
10:30
30m
Coffee break
Coffee Break
Social

11:00 - 12:30
ECMFA Session 6: Model Consistency and CollaborationECMFA at Oak
Chair(s): Jesús Sánchez Cuadrado Universidad de Murcia

Remote Participants: Zoom Link

11:00
30m
Talk
A flexible operation-based infrastructure for collaborative model-driven engineering
ECMFA
P: Edvin Herac Johannes Kepler University, Wesley Assunção Johannes Kepler University Linz, Austria & Pontifical Catholic University of Rio de Janeiro, Brazil, Luciano Marchezan , Rainer Haas Linz Center of Mechatronics GmbH, Alexander Egyed Johannes Kepler University Linz
DOI
11:30
30m
Talk
One-Way Model Transformations in the Context of the Technology-Roadmapping Tool IRIS
ECMFA
P: Florian Sihler Ulm University, Matthias Tichy Ulm University, Germany, Jakob Pietron Ulm University
DOI File Attached
12:00
30m
Talk
Towards behavioral consistency in multi-modeling
ECMFA
P: Tim Kräuter Western Norway University of Applied Sciences, Harald König University of Applied Sciences, FHDW Hannover and Western Norway University of Applied Sciences, Adrian Rutle Western Norway University of Applied Sciences, Yngve Lamo Western Norway University of Applied Sciences, Patrick Stünkel
DOI Pre-print
Questions? Use the STAF Keynotes contact form.