Develop bounded model checker for C programs that detects undefined behavior. Convert prototype developed in Phase I into a robust tool capable of analyzing Airliner, a drone autopilot developed by Windhover under contract from NASA.
The bounded model checker and a C interpreter that detects undefined behavior in unit tests are both generated from the same formal semantics of C.
Both the tools will be integrated into the build system of Airliner, and used to analyze Airliner and applications built from Airliner.
Much satellite software is written in C. For example, NASA's "core Flight Software" is written in C.
Software for unmanned aircraft systems tends to be written in C. For example, Airliner is a drone autopilot.
C is the most widely used programming language for embedded systems, and is used in the automotive industry, in telecommunications, in robotics. It is used for the infrastructure of the internet. It is the main language used for Linux. Our tools can be applied to any software written in C.