Workshop on Formal Methods For Robotics: Benchmarks and Evaluation Metrics

statement of purpose

The term "formal methods" refers broadly to techniques for the verification and automatic synthesis of systems that satisfy desirable properties exactly or within some statistical tolerance. Historically developed for concurrent software, recent work has brought these methods to bear on motion planning in robotics. Challenges specific to robotics, such as uncertainty and real-time constraints, have motivated extensions and entirely novel treatments which draw on ideas from automata theory, logic, model checking, hybrid systems and control. However, compared to other areas of robotics research, demonstrations of formal methods have been surprisingly small-scale. In addition, there is a lack of benchmarks and metrics for evaluating novel algorithms.

This half-day workshop will bring together leading researchers in robotics, formal methods and hybrid systems, including those from industry. The discussions will be focused on metrics for evaluating the state of the art of formal methods for synthesis and verification of robotic systems, including the construction of appropriate benchmarks. This workshop will build on the success of its predecessors at ICRA 2009, 2010, CAV 2011, and RSS 2013, 2014. These previous events have tended toward broad inclusion of relevant work, motivated in part by the nascency of the field. We propose to focus this manifestation of the series at ICRA 2015 on benchmarks and metrics for evaluation. It will also provide a venue for discussing preparations and results from the First Challenge on Formal Methods for Robotics.

tentative agenda

The workshop will take place during the morning of Saturday, 30 May 2015. Please beware that this agenda may change as we finalize workshop details. You may also want to consult the official schedule of workshops at ICRA 2015.

08:30-9:15 Invited talk by Peter Trautman (Galois, Inc.): Formal methods at Galois Inc: current results, ongoing work, and future challenges
09:15-10:00 Invited talk by Eric Klavins (U. Washington): Reproducible experimental workflows though protocol programming languages
10:00-10:30 coffee
10:30-11:00 panel discussion
11:00-11:16 lightning talks
11:16-11:20 voting and organizing into SIGs
11:20-11:45 SIGs (a.k.a., "special interest groups" or "birds of a feather")
11:45-12:00 summaries about ideas and plans from SIGs