Runtime Verification, Inc. SBIR Phase II Award, August 2021

Develop bounded model checker for C programs that detects undefined behavior.nbsp; 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.