Transforming Specifications into Robot Programs:
A Survey of Formal Methods Tools for Non-Experts
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, and lay the foundation for formal verification of planning components (e.g. ML). 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.
Call for Tool Demonstrations
We solicit contributed tool demonstrations. The tools will be highlighted via ~5 min lightning talks, followed by a short ~15-minute period for general feedback, and wrapping up in individual breakout sessions at tables where the tools will be demonstrated. Demonstrations should include:
- how to define a simple example to use the tool,
- a realistic example that can also be executed by interested researchers, and
- videos or demos on real robots.
The submission should be in the form of a one-page document, including:
- Abstract for the lightning talk
- Demonstration plan at the workshop
- URL for the tool
The site can be a static website or github repository that includes the tool’s name, description (abstract), purpose, authors, licensing information, and citation information. We will accept both open and closed source tools, but will require, at a minimum, that they be freely available to use and distribute for academic purposes and be accessible by all workshop participants. Acceptance will be based on: installation and dependencies, examples and reproducibility of examples, how easy it is to create new cases, API and use with other tools (e.g. ROS), documentation, and generality.
Tool demonstrations should be submitted to: firstname.lastname@example.org
Description of the event
The goal of the workshop is to facilitate the exposure of formal methods (FM) fields and tools developed in recent years for robotics to the wider community, and close the loop by soliciting feedback on these methods and software from potential non-expert users.
The workshop continues a long line of effort to bring formal methods closer to the robotics community, e.g., workshops at RSS 2013, 2014, 2015, 2017, ICRA 2015, 2016. While previous events were focused on presenting state-of-the-art research in the intersection of the two fields, the previous workshop at RSS 2017 and the current proposal focus on highlighting to the wider robotics community the benefits of formal specification and the developed state-of-the-art tools that are at the users’ disposal, respectively.
The first half of the workshop will feature a series of warmup talks to expose attendees to the wide variety of problem formulations that are currently used to solve planning problems in robotics, with and without formal specification languages.
The talks will end in a panel discussion, where we will actively drive the interaction between participants towards formulating problems and questions for short- and long-term research.
For the second half of the workshop, we will solicit contributed tool demonstrations. The tools will be highlighted via lightning talks of ~5 min. Afterwards, we will have a short ~15 minutes period for general feedback, and then the attendees will break off into tables where the tools will be demonstrated.
- Cristian-Ioan Vasile, Lehigh University, PA, USA
- Jonathan DeCastro, Toyota Research Institute, MA, USA
Contact the organizers: email@example.com, firstname.lastname@example.org
- Workshop Date: Sunday May 31st 2020 (Full Day Workshop: 8:30-17:30)
- Location: Room 324M
- Demonstration Submission Deadline: Sunday March 15th 2020
- Acceptance Notifications: Sunday April 5th 2020
- Demo Presentation Submission Deadline: Friday May 15th 2020
- Prof. Calin Belta, Boston University, USA
- Prof. Lydia Kavraki, Rice University, USA
- Prof. Hadas Kress-Gazit, Cornell University, USA
- Prof. Marco Pavone, Stanford University, USA
- Prof. Sanjit A. Seshia, University of California, Berkeley, USA
- Prof. Angela Schoellig, University of Toronto, Canada
- Prof. Dylan Shell, Texas A&M University, USA
- Prof. Russ Tedrake, Massachusetts Institute of Technology, USA
- TBD, TBD
- TBD, TBD
08:45 – 09:00 Welcome and Overview
09:00 – 10:30 Session 1: 4 talks
10:30 – 10:45 Coffee break
10:45 – 12:15 Session 2: 4 talks
12:15 – 14:00 Lunch break
14:00 – 14:40 Session 3: 2 talks
14:40 – 15:00 Panel discussion
15:00 – 15:50 Lightning session and feedback: ~8 talks
15:50 – 16:05 Coffee break
16:05 – 17:25 Demonstration and Tutorial session
17:25 – 17:30 Concluding remarks