Building a freely-available, open-source, scalable model checking infrastructure for safety-critical systems

Safety-critical and security-critical systems help fly our planes, drive our cars, deliver our packages, ensure our electricity, and even automate our homes. We increasingly rely on such systems, especially when humans cannot perform a task in person, for example due to a dangerous working environment. However, before any safety-critical system launches into the human environment, we need to be sure it is really safe. Model checking is a popular and appealing way to rigorously check for safety: with an accurate model of a system, model-checking can either prove it will always operate safely, or flag any potential safety violations before they happen. Researchers are continuously working to improve the speed and efficiency of model checking algorithms, but even as model checking becomes more integrated into the standard design process, the platforms for model checking research have become more limited. Previous options have become closed-source or industry tools; current research platforms don't have support for expressive specification languages needed for verifying real systems.

This project will fill the current gap in model checking research platforms by building a freely-available, open-source, scalable model checking infrastructure that accepts expressive models and efficiently interfaces with the currently-maintained state-of-the-art back-end algorithms to provide an extensible research and verification tool. The end result will be a community resource with a well-documented intermediate representation to enable extensibility, and a web portal, facilitating new modeling languages and back-end algorithmic advances. The infrastructure will be ideal for catapulting formal verification efforts in many cutting-edge application areas, including security, networking, and operating system verification.