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

该项目的目标是利用作为题为“计算机辅助程序工程(Expeditions)：利用合成进行软件设计”的项目的一部分开发的合成和自动推理技术，以帮助确保自动驾驶车辆的安全。自动驾驶汽车涉及感知、规划、控制和算法的组合，这些都太复杂了，无法完全验证，无法保证完全的可靠性，但目标是表明，在许多重要场景下，可以验证单个组件是否正确工作。该项目的关键创新之一是表明合成技术在这项具有挑战性的任务中发挥了作用。综合通常旨在生成一段行为满足某些约束的代码，但Exscape项目展示了综合的一个重要应用：生成适合程序分析的复杂系统的模型。在自动驾驶汽车的背景下，关键的想法是利用合成来生成特定场景的模型，例如右转或在高速公路上超车，这些场景捕捉了大量可能的场景，但足够窄，可以针对这些场景验证单个组件，从而易于处理。除了技术开发，这项工作还为参与出口工作的学生和博士后提供了与丰田的工业合作伙伴密切合作的机会，并将这些想法应用到工业环境中。

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.