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.

• 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.

• Tool Demonstration Submission Deadline: 20 August 2021 (AoE)

• Acceptance Notifications: 25 August 2021

• Presentation Submission Deadline: 05 September 2021

• Workshop Date: 01 October 2021

Talk 1

"Specifications, Synthesis, and Verification for HRI"

Speaker: Hadas Kress-Gazit

Talk 2

"An Introduction to the STLCG Toolbox"

Speaker: Marco Pavone, Karen Leung

Talk 3

"Informal Cogitations on Formalish Methods for Robotics"

Speaker: Dylan Shell

Talk 4

"Synthesis of Provably Correct Controller for Autonomous Systems: Applications and Challenges"

Speaker: Tichakorn (Nok) Wongpiromsarn

Talk 5

"Synthesis for Manipulation Domains"

Speaker: Lydia Kavraki

Talk 6

"Verified AI-Based Autonomy: A Formal Methods Perspective"

Speaker: Sanjit Seshia

Talk 7

"Formal Methods for Autonomous Driving"

Speaker: Calin Belta