LiVe 2021: 5th Workshop on Learning in Verification

held as a satellite event of ETAPS, on March 27, 2021 (together with the postponed LiVe 2020)

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 has been postponed together with ETAPS 2020 and will take place together with the 5th edition during ETAPS 2021.

Invited speakers

Invited talk will be delivered by

Martin Vechev and Matthew Mirman (ETH): Certified Deep Learning
Abstract: In this talk, we will discuss some of the latest advances in constructing provable deep neural networks, including new abstract interpretation based methods, provable defenses and going beyond local robustness by certifying generative models. More details of these and other advances can be found at: http://safeai.ethz.ch/

Informal proceedings

For participants conveneince, presentations are accompanied by the extended abstracts (2021 and 2020) which, however, are no formal publications.

Programme

The workshop takes place as a Zoom meeting on March 27, 2021 (all times CET). The breaks are held in gather.town

Session 1 Invited talk
- 09:00 - 10:00 Martin Vechev and Matthew Mirman: Certified Deep Learning
Coffee break (20 min)
Session 2 LiVe'21 (chair: Blaise Genest)
- 10:20 - 10:40 Thiago D. Simão, Nils Jansen and Matthijs T. J. Spaan: AlwaysSafe: Reinforcement Learning without Safety Constraint Violations during Training
- 10:40 - 11:00 Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe and Andrea Peruffo: Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks
- 11:00 - 11:20 Kairo Morton, William Hallahan, Elven Shum, Ruzica Piskac and Mark Santolucito: Grammar Filtering For Syntax Guided Synthesis
- 11:20 - 11:40 Nils Jansen, Steven Carr and Ufuk Topcu: Model-based Verification of Recurrent Neural Networks for Temporal Logic Constraints
- 11:40 - 12:00 Irene Vlassi Pandi, Earl T. Barr, Andrew D. Gordon and Charles Sutton: Probabilistic Type Inference by Optimizing Logical and Natural Constraints
Lunch break (60 min)
Session 3 LiVe'20 - Part I (chair: Andy Gordon)
- 13:00 - 13:20 Cedric Richter and Heike Wehrheim: Algorithm Selection with Attention on Software Verification
- 13:20 - 13:40 Jan Kretinsky, Alexander Manta and Tobias Meggendorfer: Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis
- 13:40 - 14:00 Priyanka Golia, Kuldeep S. Meel and Subhajit Roy: A Data Driven Approach for Skolem Function Synthesis
- 14:00 - 14:20 Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz and David Aspinall: Robustness as a Refinement Type
Coffee break (40 min)
Session 4 LiVe'20 - Part II
- 15:00 - 15:20 Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott Smolka and Scott Stoller: Neural Predictive Monitoring and a Comparison of Frequentist and Bayesian Approaches
- 15:20 - 15:40 Hugo Bazille, Blaise Genest, Cyrille Jegourel and Jun Sun: Global PAC Bounds for Learning Discrete Time Markov Chains
- 15:40 - 16:00 Dennis Gross, Nils Jansen and Guillermo Alberto Perez: Formally Verifying the Robustness of Multiple-Classifier Combinations

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, 2021~~ deadline extended: March 4, 2021
Notification: March 15, 2021

In case of any questions, please contact the organizer Jan Kretinsky at <name>.<surname>@tum.de

Looking forward to seeing you LiVe in Munich in 2022!