12. – 17. Februar 2017, Dagstuhl-Seminar 17071

Computer-Assisted Engineering for Robotics and Autonomous Systems


Erika Abraham (RWTH Aachen, DE)
Hadas Kress-Gazit (Cornell University – Ithaca, US)
Lorenzo Natale (Italian Institute of Technology – Genova, IT)
Armando Tacchella (University of Genova, IT)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 7, Issue 2 Dagstuhl Report
Dagstuhl's Impact: Dokumente verfügbar
Programm des Dagstuhl-Seminars [pdf]


This seminar focused on autonomous systems, and more specifically robots, that operate without, or with little, external supervision. For these systems to be integrated into society, it is highly important to make sure that they are functionally safe. Formal Methods are techniques adopted in engineering for the verification of software and hardware systems. As models are a basic requirement for the formal analysis of systems, Model-driven Software Engineering plays an important role to enable the application of Formal Methods. Though autonomous systems are increasingly involved in our everyday life, both exact formalizations of safe functionality (standards, what we want to be confident in) and methods to achieve confidence (methodologies, how we get confident in the properties we want to assure) are still scarce. This seminar brought together experts in Artificial Intelligence and Robotics, Model-driven Software Engineering, and Formal Methods. It included researchers from academia as well as from industry. The following list summarizes high-level themes that emerged from the seminar:

  • Dealing with highly complex systems, it is difficult to verify or even model all aspects of the system, therefore focusing effort on efficient falsification rather than costly verification can be highly impactful for industrial applications.
  • The community can and should leverage results and systems built for different robotic competitions to reason about possible requirements and techniques to verify/falsify them. These competitions include the DARPA robotics challenge, the Amazon picking challenge, different leagues in Robocup, etc. Creating benchmarks based on these competitions will enable progress in verification of autonomous systems.
  • Creating small interdisciplinary teams that include people from formal methods, robotics and model based design that tackle small yet realistic problems, possibly inspired by industrial applications, will help formalize the language of requirements, models and verification techniques that will have an impact on autonomous systems.
Summary text license
  Creative Commons BY 3.0 Unported license
  Erika Abraham, Hadas Kress-Gazit, Lorenzo Natale, and Armando Tacchella


  • Artificial Intelligence / Robotics
  • Software Engineering
  • Verification / Logic


  • Autonomous Systems
  • Artificial Intelligence
  • Robotics
  • Computer-aided Software Development
  • Domain-specific Languages
  • Model-driven Software Engineering
  • Safety
  • Testing
  • Analysis
  • Verification
  • Synthesis
  • Formal Methods


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.