Formal methods - mathematical techniques for describing systems, capturing requirements, and providing guarantees - have been used to synthesize robot control from high-level specification, and to verify robot behavior. Given the recent advances in robot learning and data-driven models, what role can, and should, formal methods play in advancing robotics? In this talk I will give a few examples for what we can do with formal methods, discuss their promise and challenges, and describe the synergies I see with data-driven approaches.
Bio: Hadas Kress-Gazit is the Geoffrey S.M. Hedrick Sr. Professor at the Sibley School of Mechanical and Aerospace Engineering at Cornell University, and the Associate Dean for Diversity and Academic Affairs of Cornell’s College of Engineering. She received her Ph.D. in Electrical and Systems Engineering from the University of Pennsylvania in 2008 and has been at Cornell since 2009. Her research focuses on formal methods for robotics and automation and more specifically on synthesis for robotics - automatically creating verifiable robot controllers for complex high-level tasks. Her group explores different types of robotic systems including modular robots, soft robots and swarms and synthesizes ideas from different communities such as robotics, formal methods, control, hybrid systems and computational linguistics. She received an NSF CAREER award in 2010, a DARPA Young Faculty Award in 2012, Cornell Engineering’s Excellence in teaching award in 2013 and 2019, and excellence in research award in 2021. She is an IEEE Fellow and has served on DARPA’s Information Science and Technology study group (ISAT), as the program chair for Robotics: Science and Systems (RSS) 2018, the program chair for the International Conference on Robotics and Automation (ICRA) 2022, and the president of the RSS board (2019-2023), among other leadership positions in the robotics community.