Artificial Intelligence (AI) techniques are increasingly being adopted in several application domains, including systems deployed in business-critical and safety-critical scenarios. However, to be really usable and eective 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 goal of this 3rd Workshop on Artificial Intelligence and f Ormal VERification, Logic, Automata, and sYnthesis (OVERLAY) is to continue a stable, long-term scientific forum on relevant topics connected to the relationships between Formal Methods and Artificial Intelligence. The workshop is sponsored by the OVERLAY research group (https://overlay.uniud.it), an ensemble of Italian researchers covering a diverse set of disciplines from both communities.
This year edition was held on September 22, 2021, and has been co-located with GandALF 2021 (12th International Symposium on Games, Automata, Logics, and Formal Verification) in Padova, Italy. Due to the unfortunate COVID-19 situation, the event has been held as a hybrid conference, with both physical and virtual participation worldwide.
Twenty papers were selected and presented during the workshop, showing an increased participation despite the general slowdown in research activities caused by the previous lockdown months. The topics of the submitted contributions range from logic to hybrid systems, from automated reasoning to machine learning, from model checking to automated planning. Interestingly, we also collected contributions studying the connection between deductive approaches and learning-based ones.
The program was also enriched by the invited talk (shared with GandALF 2021) by Roderick Bloem (Institute of Applied Information Processing and Communications, Graz, Austria), titled “Shield Synthesis for Safe Reinforcement Learning”, whose presentation focused on methods to use reactive synthesis to construct runtime enforcement modules (shields) that can ensure that a system works correctly, even if it has bugs. An extended abstract summarizing Bloem’s contribution to the workshop starts this volume.
The workshop provided a stimulating environment where researchers from both the AI and FM communities gave rise to lively discussions on current opportunities and challenges. 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 towards 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 Roderick Bloem, and all the program committee members. We would also like to thank the GandALF organizers, Davide Bresolin and Pierre Ganty, for hosting our workshop and sharing the invited speaker. Last, but not least, we want to add a gigantic thank to Gigante Nicola, for his enormous help in several aspects such as logistics, website, editorship, and much more. The workshop chairs,