A Scalable Semantics-Based Verification System for Flight Critical Software

Flight-critical systems rely on an ever increasing amount of software—the Boe- ing 777 contains over 2 million lines of code. Most of this code is written in the C programming language. We need a scalable static formal program verification tool that is able to prove the functional correctness of flight-critical software, limiting any failure of flight critical software to hardware faults. This project seeks to leverage the matching logic verification framework. Matching logic is generic in an operational semantic of a given programming language, so we also seek to give a semantics of a subset of C, called CIL, which is guaranteed to be deterministic. While we already have a semantics for the entirety of C, CIL is more representative of flight-critical software, and the simpler, deterministic semantics will result in a more efficient, and thus more scalable, static program verification tool. We are also building a new unification- based rewrite engine that will result in a more powerful version of the Matching Logic Framework. In order to make the tool more commercially feasible, we will develop new techniques in pattern inference, so that loop invariants and some pre/post conditions can be determined automatically. We will perform a thorough evaluation of our tool on a large-scale piece of software with similar characteristics to a flight system.