InTrans: TRI-MIT Collaboration on Formal Verification Meets Big Data Intelligence in the Trillion Miles Challenge

点击翻译按钮获取中文摘要

The goal of this project is to leverage the Synthesis and automated reasoning techniques developed as part of the project titled "Expeditions in Computer Aided Program Engineering (ExCAPE): Harnessing Synthesis for Software Design" in order to help ensure the safety of self driving vehicles. Self-driving vehicles involve a combination of perception, planning, control and algorithms that are too complex to be fully verified to guarantee complete reliability, but the goal is to show that individual components can be verified to work correctly under many important scenarios. One of the key innovations in this project is to show that synthesis technology has a role to play in this challenging task. Synthesis generally aims at generating a piece of code whose behavior satisfies some constraints, but the ExCAPE project demonstrated an important application of synthesis: generating models of complex systems that are amenable to program analysis. In the context of self-driving cars, the key idea is to leverage synthesis to generate models of particular scenarios, such as making a right turn or passing a car in a freeway, that capture a large space of possible situations, but are narrow enough for verification of individual components against those scenarios to be tractable. In addition to the technology development, the work provides the opportunity for students and postdocs who were involved in the ExCAPE effort to collaborate closely with our industrial partners at Toyota and apply these ideas in an industrial setting.