Welcome
Welcome to the website of the OVERLAY research group on Formal Methods for AI.
The OVERLAY group (acronym for fOrmal VERification, Logic, Automata, and sYnthesis) fosters the collaboration among a diverse team of Italian researchers in the fields of Formal Methods and Artificial Intelligence, aiming at pursuing multidisciplinary research at the border of the two fields.
Among its activities, the group organizes the OVERLAY workshop, an annual event promoted to highlight the most recent developments at the border of the two fields and promoting cross-dissemination between researchers.
The last edition of the OVERLAY workshop took place in Rome on November 7th, 2023, as part of the AIxIA conference. See all the details on the workshop page.
Latest news
The proceedings of the OVERLAY 2023 workshop are online!
Thematic areas
The activities of the group are categorised into four thematic areas which summarise the different research topics of the group's members.
Automated Planning
Coordinator: Alfonso Gerevini
Automated Planning is one of the cornerstone fields of Artificial Intelligence, being actively studied since the '60s.
The purpose of automated planning research is to develop formally well-founded and domain-independent techniques and methods to design agents that can pursue their goal while interacting with their environment.
The domain-independence of these techniques is the main advantage — and the main source of hardness — of AI planning, whose methods can be employed and adapted to a great variety of domains, in contrast to the development of ad-hoc algorithmic techniques for the specific problem at hand.
In this thematic area, great emphasis is given to the formal foundations of planning techniques, which have to guarantee to find a correct strategy to pursue the given goal, making AI planning a central component of any trustworthy AI infrastructure.
Formal Methods
Coordinator: Adriano Peron
The development of complex system deployed in business-critical or safety-critical scenarios need to be approached with care as to avoid irreparable incidents.
For this reason, many techniques have been devised in the last decades to help ensuring the highest possible levels of safety and trust in the development of such systems.
The Formal Methods field encompass a great variety of methods, tools, and techniques to model complex systems, studying their behavior, check their correctness with respect to formal specifications, or synthesize correct-by-construction implementations base on such specifications.
In this thematic area, particular attention is devoted to the application of such techniques to artificial intelligence systems, that by the nature of their applications most require safety assurance.
Discrete and continuous hybrid systems
Coordinator: Tiziano Villa
Complex systems, including those driven by artificial intelligence technologies, do not often operate in isolation but interact with the physical world. When the interaction with the environment involves continuous physical phenomena, the formal tools and techniques used to model, verify, and synthesise such systems change drastically, entering the realm of Cyber-Physical Systems (CPSs).
By their nature, CPSs are often employed in safety-critical scenarios. It is thus crucial to study how such system can be modeled and verified.
In this thematic area, Cyber-Physical Systems are studied in their connection with complex systems guided by artificial intelligence, to study and develop techniques ensure their safety and trustability.
Tools and applications
Coordinator: Alessandro Cimatti
Fundamental research in the thematic areas outlined above needs a strong committment to the development of efficient algorithms and robust software tools, to evaluate the feasibility of the approaches and transfer the result of the research to industry and society.
The connection with industry is fundamental not only to apply basic research but also to identify new problems, use cases, and research challenges that drive novel research developments, in a virtuous cycle that benefits all.
In this thematic area, attention is put on the development of strong tools deriving from fundamental research in AI and Formal Methods, and how such tools can be applied to real-world needs of industry and society.