LiVe 2023: 7th Workshop on Learning in Verification
- Held as a satellite event of ETAPS'23 in Paris, on April 22, 2023
Topic
The success of machine learning has recently motivated 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 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).
Invited speaker
Invited talk will be delivered by
Thiago D. Simão
Preliminary programme
The workshop takes place on site in the room Hermite (the largest of all workshop rooms) of the Institut Henri Poincaré, 11 Rue Pierre et Marie Curie, Paris, France,
on April 22, 2023 (all times CEST).
The inofficial proceedings with all abstracts can be found here.
The talks are planned 15 minutes long plus 5-10 minutes discussion.
- Session 1 (9:00 - 10:00)
- Charlie Molony and Vasileios Koutavas: Towards a Machine Learning Approach for the Detection of Null Pointer Errors
-
Andoni Rodriguez, César Sánchez and Felipe Gorostiaga: Formal verification of loss-functions: quality assessment in image super-resolution
-
Jan Kretinsky, Maximilian Prokop, Tobias Meggendorfer and Sabine Rieder: Guessing Winning Policies in LTL Synthesis by Semantic Learning
Coffee break
- Session 2 (10:30 - 12:30, NN)
- Eric Alsmann, Marco Sälzer, Florian Bruse, Rüdiger Ehlers and Martin Lange: Translating Neural Networks Into IO-Equivalent Finite Automata
- Guy Amir, Davide Corsi, Raz Yerushalmi, Luca Marzari, Alessandro Farinelli, David Harel and Guy Katz: Verifying Learning-Based Robotic Navigation Systems
- Calvin Chau, Stefanie Mohr and Jan Křetínský: Semantic Abstraction of Neural Networks
- Shahaf Bassan and Guy Katz: Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
- Marco Sälzer and Martin Lange: About Limits In Formal Verification of Graph Neural Networks
Lunch break
- Session 3 (14:00 - 16:00, RL I)
- 14:00 - 15:10
Invited talk - Thiago D. Simão
- Pedro R. D'Argenio, Juan Andres Fraire, Arnd Hartmanns and Fernando Raverta: On Q-Learning Routes in Uncertain Delay-Tolerant Networks
- Mahsa Varshosaz, Mohsen Ghaffari, Einar Broch Johnsen and Andrzej Wasowski: Towards Formal Specification of Reinforcement Learning
Coffee break
- Session 4 (16:30 - 18:00, RL II)
- Avraham Raviv, Eliya Bronshtein, Or Reginiano, Michelle Aluf-Medina and Hillel Kugler Learning Through Imitation by using Formal Verification
- Marnix Suilen, Thiago D. Simão and Nils Jansen Safe Policy Improvement for POMDPs
- Muqsit Azeem, Alexandros Evangelidis, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr and Maximilian Weininger: 1-2-3-Go! Explainable Policies for Arbitrarily Large Parametrized Markov Decision Processes via Decision-Tree Generalization
- Discussion
Self-supported workshop dinner
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 1, 2023 deadline extended: March 8, 2023
- Notification: March 15, 2023
- Final versions for informal pre-proceedings: March 30, 2023
In case of any questions, please contact the organizer Jan Kretinsky at <name>.<surname>@tum.de
Looking forward to seeing you LiVe!