Title: Applications of Formal Methods to Practical Problems
Date: Thursday, March 3, 2016
Time: 10:00 – 11:00
Room: 137, NIA
Speaker: Srinivas Nedunuri
Abstract: Briefly survey a couple of examples of where formal methods can aid in solving practical problems and then delve into one example in more detail, namely programming robots. The goal of the Robosynth project is to synthesize programs from programmer supplied plan outlines, freeing the programmer from having to specify the details. The project introduced several novel ideas, including a DSL for writing plan outlines, a solution method based on verification conditions and SMT solvers, and a scalable way of representing a continuous motion space to the solver. The talk will also briefly touch on the synthesis of reactive plans from temporal specifications.
Bio: Srinivas Nedunuri spent over 10 years in the tech industry as a software engineer before returning to UT Austin to get his PhD in the area of program synthesis from formal specifications, specifically synthesizing efficient search algorithms for near-greedy problems. Following that he worked as a postdoctoral research associate in a joint formal methods/robotics project and then as a researcher at an AI company.