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 Reports
As part of the mandatory documentation, participants are asked to submit their talk abstracts, working group results, etc. for publication in our series Dagstuhl Reports via the Dagstuhl Reports Submission System.
- Upload (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)
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.
- Eric Atkinson (Binghamton University, US)
- Joydeep Biswas (University of Texas - Austin, US) [dblp]
- Wendelin Böhmer (TU Delft, NL)
- Jonathan DeCastro (Toyota Research Institute - Cambridge, US) [dblp]
- Clemens Dubslaff (TU Eindhoven, NL)
- Khen Elimelech (Rice University - Houston, US) [dblp]
- Georgios Fainekos (Toyota Motor North America, R&D - Ann Arbor, US) [dblp]
- Maris Galesloot (Radboud University Nijmegen, NL)
- Anna Gautier (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Kush Grover (TU München, DE)
- Sofie Haesaert (TU Eindhoven, NL) [dblp]
- 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) [dblp]
- Sydney Katz (Stanford University, US)
- Michaela Klauck (Robert Bosch GmbH - Stuttgart, DE) [dblp]
- Mykel Kochenderfer (Stanford University, US) [dblp]
- Johannes Köhler (ETH Zürich, CH)
- Jan Kretinsky (Masaryk University - Brno, CZ) [dblp]
- Hanna Kurniawati (Australian National University - Canberra, AU) [dblp]
- Bruno Lacerda (University of Oxford, GB) [dblp]
- Lars Lindemann (USC - Los Angeles, US) [dblp]
- Sara Magliacane (University of Amsterdam, NL) [dblp]
- Dimitra Panagou (University of Michigan - Ann Arbor, US) [dblp]
- David Parker (University of Oxford, GB) [dblp]
- Karinne Ramirez Amaro (Chalmers University of Technology - Göteborg, SE) [dblp]
- Christian Schilling (Aalborg University, DK) [dblp]
- Philipp Schillinger (Bosch Center for AI - Renningen, DE) [dblp]
- Thiago D. Simão (TU Eindhoven, NL) [dblp]
- Stephen Smith (University of Waterloo, CA) [dblp]
- 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) [dblp]
- Abhinav Verma (Pennsylvania State University - University Park, US) [dblp]
- Esen Yel (Rensselaer Polytechnic Institute, US) [dblp]
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