LiVe 2017: 1st Workshop on Learning in Verification
- satellite event of ETAPS 2017 on April 29, 2017, in Uppsala, Sweden
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), or meta-usage of machine learning (e.g. to predict the best tools to be applied to a verification problem).
Programme
List of accepted presentations (alphabetically)
- Alessandro Abate:
Data-driven and model-based formal verification of complex physical systems
- Dalal Alrajeh, Susmit Jha and Sanjit Seshia:
A Non-monotonic Theory of Oracle-guided Inductive Synthesis
- Oana Andrei, Muffy Calder, Matthew Chalmers, Alistair Morrison and Mattias Rost:
Probabilistic Formal Analysis of a Mobile App Usage to Inform Redesign
- Pranav Ashok, Jan Kretinsky and Tobias Meggendorfer:
Learning-based Analysis of Markov Decision Processes: Reachability, LTL, and Mean Payoff
- Luca Bortolussi:
Machine Learning for Model Abstraction
- Tomas Brazdil, Krishnendu Chatterjee, Jan Kretinsky and Viktor Toman:
Strategy Representation by Decision Trees
- Mike Czech, Eyke Huellermeier, Marie-Christine Jakobs and Heike Wehrheim:
Predicting Rankings of Software Verification Competitions
- Gerco van Heerdt, Matteo Sammartino and Alexandra Silva:
CALF: Categorical Automata Learning Framework
- Nils Jansen, L. Murat Cubuktepe and Ufuk Topcu:
Synthesis of Shared Control Protocols with Provable Safety and Performance Guarantees
- Tom Janson and Sebastian Junges:
Integrating Machine Learning and Model Checking for Model Repair
- Marco Muniz, Kim Guldstrand Larsen and Jakob Haahr Taankvist:
Uppaal Stratego for Intelligent Traffic Lights
- Daniel Neider:
ICE Learning: An Overview
Invited talk will be delivered by
- Kim G. Larsen (Aalborg University, Denmark), an ERC Advanced Grantee with project LASSO (Learning, analysis, synthesis and optimization of cyber-physical systems)
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 3, 2017
- Notification: February 21, 2017
- Final versions for informal pre-proceedings: March 1, 2017
PC chairs
In case of any questions, please contact the organizer Jan Kretinsky at <name>.<surname>@tum.de
Looking forward to seeing you LiVe in Uppsala!