IROS 2021 workshop on

Transforming Specifications into Robot Programs:

A Survey of Formal Methods Tools for Non-Experts

October 1st, 2021 (Virtual)

Overview

The formal methods community has produced many successful results and tools in computer science, and over the past two decades has initiated a steady effort in moving towards applications in robotics. However, most researchers and practitioners in robotics are unaware of or find it difficult to adopt these methods due to: 1) the high initial effort to use, and 2) a disconnect between the method and tool developers and the larger community. While initially methods were shown in simple proof-of-concept scenarios, today, tools have matured to conform to the requirements of robotics applications. These tools offer the logical reasoning necessary to automate the planning and control programs, provide a-priori guarantees (certificates) for bug-free achievement of tasks, provide unambiguous specification languages for users, lay the foundation for formal verification of planning components (e.g. machine learning approaches), provide a framework for explainable deep learning, and enable embedding of logical structure in learned models. This workshop seeks to bring together the robotics and formal methods communities in a hands-on event that will demystify the current state-of-the-art, bridge the knowledge-transfer gap, and foster continued collaboration between the communities. We aim to encourage roboticists to adopt and include in their research automated synthesis and formal verification tools, and direct the formal methods community to the needs of robotics practitioners.

Objectives

To create a survey of tools within the formal methods community that will materialize into a repository of curated tools, and a survey paper in a leading robotics journal;
To increase the visibility of existing tools and lower the barriers of entry for non-expert and starting researchers and students; curated tools presented during the workshop and collected afterwards will be assessed with respect to multiple measures of maturity (e.g., stability, repeatability, documentation, tutorials, demonstrations, maintenance, etc.);
To define research and development tracks that foster wider adoption of formal methods in robotics.