Preface

Artificial Intelligence (AI) techniques are increasingly being adopted in ever more application domains,
including systems deployed in business-critical and safety-critical scenarios. However, to be really usable
and effective for these applications, AI systems have to be designed with reliable, robust and verifiable
methodologies. Since these have been the core mission of the Formal Methods (FM) community for decades,
encouraging a fruitful interaction between AI and FM researchers is becoming every day more necessary.
    The main goal of this First Workshop on Artificial Intelligence and fOrmal VERification, Logic,
Automata, and sYnthesis (OVERLAY) is to establish a stable, long-term scientific forum on relevant topics
connected to the relationships between Formal Methods and Artificial Intelligence. The workshop has
been the first official initiative sponsored by the OVERLAY research group (https://overlay.uniud.it),
an ensemble of Italian researchers covering a diverse set of disciplines from both communities. The
18th International Conference of the Italian Association for Artificial Intelligence (AI*IA 2019), which
hosted the workshop, was the perfect setting to bootstrap the initiative and to present the newly-formed
group to the Italian AI research community.
    In its two afternoons of technical program, the workshop provided a stimulating environment where
researchers from both areas discussed current opportunities and challenges. Sixteen papers have been
selected and presented during the workshop, spanning from logic to hybrid systems, from formal verification
to automated planning, from model checking to machine learning. The program was also enriched by the
invited talk by Alessandro Abate (Oxford University, UK), «Certified Reinforcement Learning with Logic
Guidance», which has been distilled into the invited contribution that starts this volume.
    The research topics and the results collected in these proceedings illustrate the work of an active and
multidisciplinary research community and confirm the growing interest for a forum where FM and AI
researchers can find a common ground.
    We would like to thank all those who made this initiative possible, starting from the authors of the
contributed papers, the invited speaker Alessandro Abate, and all the program committee members. We
would also like to thank AI*IA and the AI*IA 2019 organizers for hosting our workshop. Finally, we are
pleased to acknowledge partial financial support by the Mathematics Department «Tullio Levi-Civita» of
the University of Padova, for which a special thank goes to Davide Bresolin.



The workshop chairs,
Nicola Gigante
Federico Mari
AndreA Orlandini