Dagstuhl Seminar 24361
Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy
( Sep 01 – Sep 06, 2024 )
Permalink
Organizers
- Nils Jansen (Ruhr-Universität Bochum, DE)
- Mykel Kochenderfer (Stanford University, US)
- Jan Kretinsky (Masaryk University - Brno, CZ)
- Jana Tumova (KTH Royal Institute of Technology - Stockholm, SE)
Contact
- Andreas Dolzmann (for scientific matters)
- Simone Schilke (for administrative matters)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
- Upload (Use personal credentials as created in DOOR to log in)
AI is a disruptive force. With growing applications in fields like healthcare, transportation, game playing, finance, or robotics in general, AI systems and methods are entering our everyday lives. Such tight interaction with AI requires serious safety, correctness, and reliability considerations. Recently, the field of safety in AI has triggered a vast amount of research.
The area of formal methods (FM) offers structured and rigorous ways to reason about the correctness of a system. Techniques range from model learning, over testing to formal verification. As an example for the application of verification in AI, solving techniques like SAT or SMT solving help to assess the robustness of neural networks. Model checking is a prominent verification technique that proves the system's correctness with respect to formal specifications.
In 2018, the time was right to bring the two communities of machine learning and formal methods together and let people discover common interests and problems. This was the aim of the Dagstuhl Seminar "Machine Learning and Model Checking Join Forces" (18121), topically a predecessor of this seminar. Now, the time is right to take the next step.
From a vast number of funded research projects and publications, it is clear that what is actually missing is a practical stance toward reliable autonomy. Building upon various collaborations and results stemming from the former seminar, we take a broader stance on AI and FM and invite key players in robotics to this Dagstuhl Seminar, in addition to a broad selection of AI and FM researchers. In particular, most of the invitees are not restricted to one research community but usually publish across several of these areas.
Via a diverse program with ample space for open yet guided discussion, we aim to address a number of key challenges that range across all fields, for instance
- specific properties of real-world problems,
- guarantees on reliability of AI systems and AI methods,
- specifications for the behavior of AI systems, and
- the form or representation of, for instance, controllers of an AI system.
![Copyright](https://www.dagstuhl.de/_Resources/Static/Packages/Dagstuhl.Site/Frontend/images/licenses/copy.png?bust=22575bbf)
- Dalal Alrajeh (Imperial College London, GB) [dblp]
- Joydeep Biswas (University of Texas - Austin, US) [dblp]
- Michael Carbin (MIT - Cambridge, US) [dblp]
- Georgia Chalvatzaki (TU Darmstadt, DE)
- Jonathan DeCastro (Toyota Research Institute - Cambridge, US)
- Khen Elimelech (Rice University - Houston, US)
- Georgios Fainekos (Toyota Research Institute North America- Ann Arbor, US) [dblp]
- Anna Gautier (KTH Royal Institute of Technology - Stockholm, SE)
- Sofie Haesaert (TU Eindhoven, NL)
- Nick Hawes (University of Oxford, GB) [dblp]
- Nils Jansen (Ruhr-Universität Bochum, DE) [dblp]
- Sebastian Junges (Radboud University Nijmegen, NL) [dblp]
- Ruya Karagulle (University of Michigan - Ann Arbor, US)
- Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
- Michaela Klauck (Robert Bosch GmbH - Stuttgart, DE)
- Mykel Kochenderfer (Stanford University, US)
- Jan Kretinsky (Masaryk University - Brno, CZ) [dblp]
- Hanna Kurniawati (Australian National University - Canberra, AU) [dblp]
- Bruno Lacerda (University of Oxford, GB) [dblp]
- Morteza Lahijanian (University of Colorado - Boulder, US) [dblp]
- Kim Guldstrand Larsen (Aalborg University, DK) [dblp]
- Lars Lindemann (USC - Los Angeles, US)
- Sara Magliacane (University of Amsterdam, NL)
- Laura Nenzi (University of Trieste, IT) [dblp]
- Dimitra Panagou (University of Michigan - Ann Arbor, US)
- David Parker (University of Oxford, GB) [dblp]
- Karinne Ramirez Amaro (Chalmers University of Technology - Göteborg, SE)
- Kristin Yvonne Rozier (Iowa State University - Ames, US) [dblp]
- Christian Schilling (Aalborg University, DK)
- Philipp Schillinger (Bosch Center for AI - Renningen, DE)
- Sanjit A. Seshia (University of California - Berkeley, US) [dblp]
- Thiago D. Simão (TU Eindhoven, NL)
- Stephen Smith (University of Waterloo, CA)
- Matthijs Spaan (TU Delft, NL) [dblp]
- Hazem Torfah (Chalmers University of Technology - Göteborg, SE) [dblp]
- Jana Tumova (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Cristian Ioan Vasile (Lehigh University - Bethlehem, US)
- Esen Yel (Rensselaer Polytechnic Institute, US)
Related Seminars
- Dagstuhl Seminar 18121: Machine Learning and Model Checking Join Forces (2018-03-18 - 2018-03-23) (Details)
Classification
- Artificial Intelligence
- Formal Languages and Automata Theory
- Robotics
Keywords
- Formal Verification
- Artificial Intelligence
- Machine Learning
- Autonomous Systems
- Robotics