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.
Key Dates
Tool Demonstration Submission Deadline:20 August 2021(AoE)Acceptance Notifications:25 August 2021Presentation Submission Deadline:05 September 2021Workshop Date: 01 October 2021
Speakers
Boston University
Rice University
Cornell University
Stanford University
and University of Washington
Stanford University and NVIDIA
University of California at Berkeley
Texas A&M University
Iowa State University
Invited Talks
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