February 12 – 17 , 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)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 7, Issue 2 Dagstuhl Report
Aims & Scope
List of Participants
Dagstuhl's Impact: Documents available
Dagstuhl Seminar Schedule [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 the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.