Formal Verification of Autonomous Systems

This project, a collaborative effort between the School of Computer Science at Carnegie Mellon University and the Automated Software Engineering Group at NASA Ames Research Center, is developing tools and techniques to support formal verification of autonomous systems. The goal is to make formal verification, and model checking in particular, easy enough to use, and powerful enough, so that it can be employed as a regular part of developing autonomous system. The hope is that by verifying early in the development cycle, subsequent testing and debugging can be significantly reduced, leading to autonomous systems that are more reliable and easier to develop.