The Formula Factory — Department of Commerce SBIR Phase I: 9.03.01.77-R

Description

Galois will build a practical, efficient, modular, deductive code verifier and verification methodology for multithread C11 software. The verifier will take code written to the C11 standard, suitably annotated with function contracts, assertions, program/data invariants, ghost data/code, and any platform-specific assumptions beyond those guaranteed by the standard, and will prove that the code meets its specifications in any suitable concurrent context. The most innovative aspect of the verifier lies in the method for reasoning about C11 weak memory atomics, the most important feature of C11. This approach allows the use of traditional forms of program reasoning using assertions about the global state (e.g. in pre/postconditions, loop and data invariants, etc.). This is done with the help of separation logic, which provides a natural approach to guaranteeing that threads interact with each other in a reasonable way. If our software is going to be used to verify high-assurance programs, the system should be high assurance as well. Therefore, the verifier will be written in the Coq proof assistant language, using the proof assistant to show the correctness of the implementation.