LiVe 2018: 2nd Workshop on Learning in Verification

a satellite event of ETAPS in Thessaloniki, Greece, April 20, 2018

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).

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).

Invited speakers

Invited talks will be delivered by

Guy Katz (Hebrew University, formerly at Stanford), co-author of Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Krishnamurthy Dvijotham (Dj) (Google DeepMind) and Pushmeet Kohli (Google DeepMind, former Machine Learning advisor to the Chief Research Officer of Microsoft)

The invitations were only possible due to the support by the European Network for Game Theory GAMENET, which is a COST Action funded project (CA 16228). COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks.

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 28, 2018~~ deadline extended March 15, 2018
Notification: March 27, 2018
Final versions for informal pre-proceedings: April 6, 2018

PC chairs

Joost-Pieter Katoen, RWTH Aachen University, Germany / University of Twente, Netherlands
Jan Kretinsky, Technical University of Munich, Germany

Programme

8.00 Registration opens
08.30 - 09.00 Welcome
09.00 - 10.00 Invited Talk: Guy Katz - Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
10.00 - 10.30 Coffee Break
10.30 - 12.30 Session 1
Georgios Giantamidis, Stylianos Basagiannis and Stavros Tripakis: Learning Symbolic DFAs from Safety LTL Properties
Mark Santolucito, Ruzica Piskac and Ennan Zhai: Using Machine Learning to Synthesize Specifications for Configuration Files
Guillermo Perez : Minimizing Regret in Infinite-Duration Games Played on Graphs
12.30 - 14.00 Lunch
14.00 - 16.00 Session 2
Invited Talk: Krishnamurthy Dvijotham, Pushmeet Kohli (Google DeepMind): Towards Verifying Neural Networks
Simone Silvetti: An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems
16.00 - 16.30 Coffee Break
16.30 - 18.00 Session 3
Pranav Ashok, Tomas Brazdil, Jan Kretinsky and Ondrej Slamecka: Monte-Carlo Tree Search in Verification of Markov Decision Processes
Final discussion

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

Looking forward to seeing you LiVe in Thessaloniki!