LiVe 2024: 8th Workshop on Learning in Verification
- Held as a satellite event of ETAPS'24 in Luxembourg, on April 6, 2024
Topic
The success of machine learning has been motivating researchers in formal methods to adapt the highly scalable learning methods to the verification setting, where correctness guarantees on the result are essential.
The aim of this workshop is to bring together researchers from the formal verification community that are developing approaches to exploit learning methods in verification or to verify systems with learning-based components as well as researchers from machine learning area interested in applications in verification and synthesis.
The general topic of machine learning in verification includes, for instance,
-
the use of learning techniques (e.g. reinforcement learning) for speeding up verification (e.g. rigorous analysis of complex systems combining non-determinism, stochasticity, timing etc.),
-
the use of machine learning data structures and algorithms (e.g. decision trees) for enhancing results of verification (e.g. generating simple invariants of programs generating small controllers of systems),
-
verification of machine-learning artefacts (e.g. verification of neural networks), or
- meta-usage of machine learning (e.g. to predict the best tools to be applied to a verification problem).
Previous editions
The 1st edition was held as a satellite event of ETAPS 2017 on April 29, 2017, in Uppsala, Sweden.
It featured 12 presentations and an invited talk by Kim G. Larsen (Aalborg University), who has an ongoing ERC Advanced Grant LASSO (Learning, analysis, synthesis and optimization of cyber-physical systems).
The 2nd edition was held as a satellite event of ETAPS 2018 on April 20, 2018, in Thessaloniki, Greece.
Apart from regular presentations, it featured two invited talks by Guy Katz (Stanford / Hebrew University) and Krishnamurthy Dvijotham (Google DeepMind) on verifying neural networks.
The 3rd edition was held as a satellite event of ETAPS 2019 on April 6, 2019, in Prague, Czech Republic. It included invited talks by Bettina Könighofer and Kristian Kersting and industrial talks by Martin Neuhäusser (Siemens) and Vahid Hashemi (AUDI).
The 4th edition had been postponed together with ETAPS 2020 and took place together with the 5th edition during ETAPS 2021 on March 27, 2021, as a virtual meeting. The invited was delivered by Martin Vechev and Matthew Mirman (both ETH Zurich).
The 6th edition was held as a satellite event of ETAPS 2022 (which we also organized) on April 2, 2022, in Munich, Germany. It featured an invited talk by Armando Tacchella (University of Genoa).
The 6th edition was held as a satellite event of ETAPS 2023 on April 22, 2023, in Paris, France. It featured an invited talk by Thiago D. Simão (Radboud University Nijmegen).
Invited speaker
Bernhard Steffen: Malwa: A Tool for Fully Automated Model Inference of Instrumented Web Applications
Abstract:
We present Malwa, our web-based tool that allows the fully automatic inference
of behavioral models from adequately instrumented web applications via active
learning. Characteristic for MALWA is its underlying domain-specific language
for HTML instrumentation that allows one to systematically construct web
applications that are learnable by design. The impact of this approach will
be illustrated along an application scenario where the code for the process
logic of the application has been generated by Chat GPT.
Preliminary programme
The workshop takes place on site in the room Schengen I of Parc Hotel Alvisse, 120 Rte d'Echternach, 1453 Dommeldange, Luxembourg,
on Saturday, April 6, 2024.
The inofficial proceedings with all abstracts can be found here.
The talks are planned 20 minutes long plus 10 minutes discussion.
Welcome and invited talk
- 9:00 Bernhard Steffen, Marco Krumrey, Alexander Bainczyk and Daniel Busch: Malwa: A Tool for Fully Automated Model Inference of Instrumented Web Applications
slides
10:00-10:30 Coffee break
Session 1: Learning policies
- 10:30 Florent Delgrange, Ann Nowe and Guillermo Perez: Distillation of RL Policies through Bisimilar Latent Models with Formal Guarantees
slides
- 11:00 Roman Andriushchenko, Alexander Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen and Filip Macák: Advances in SAYNT: Symbiotic Policy Synthesis in POMDPs
slides
- 11:30 Andoni Rodriguez and César Sánchez: Towards Adaptive Reactive Synthesis Modulo Theories (Extended Abstract)
- 12:00 Debraj Chakraborty, Clemens Dubslaff, Sudeep Kanav, Jan Kretinsky and Christoph Weinhuber: Predicate Decision Diagrams for Explainable Policy Representation
slides
12:30-14:00 Lunch break
Session 2: Automata learning
- 14:00 Anirban Majumdar, Sayan Mukherjee and Jean-François Raskin: Learning Event-recording Automata Passively
- 14:30 Simon Dierl and Falk Howar: MILP Formulations for Passive Learning
- 15:00 Gaëtan Staquet: Validating JSON Documents with Learned Visibly Pushdown Automata
- 15:30 (short talk) Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretínský, Stefanie Mohr:
Learning Explainable and Better Performing Representations of POMDP Strategies
15:45-16:30 Coffee break
Session 3: Neural networks the times have been updated to align with the coffee break
- 16:30 Gesina Schwalbe, Christian Wirth and Ute Schmid: Enabling Verification of Deep Neural Networks in Perception Tasks Using Fuzzy Logic and Concept Embeddings
- 17:00 Stefanie Mohr, Muqsit Azeem, Jan Kretinsky, Sudeep Kanav, Sabine Rieder and Marta Grobelna: Monitizer: Automating Design and Evaluation of Neural Network Monitors
- 17:30 Rong Gu: Integrating the Power of Machine Learning and Model Checking in Safety-Critical Systems
- Discussion
Self-supported workshop dinner: We gather 18:30 in the lobby
Submissions
Since the aim of the workshop is to stimulate discussion on the potential of learning techniques in verification and to report on recent advancements, we invite presentations of possibly already published as well as ongoing work.
The submissions should be abstracts of such work, limited to at most two pages in the llncs style, and will only be published in the informal pre-proceedings for the convenience of the participants. There will be no formal publication or post-proceedings.
The submission are to be done over Easychair.
Important dates:
- Paper submission: February 24, 2024
- Notification: March 4, 2024 (early registration deadline is March 6)
- Final versions for informal pre-proceedings: March 18, 2024
In case of any questions, please contact the organizer Jan Kretinsky at <name>.<surname>@tum.de
Looking forward to seeing you LiVe!