A Verifier for Multicore C11 or C++11 Code

Period of Performance: 01/01/2015 - 12/31/2015


Phase 1 SBIR

Recipient Firm

Formula Factory
107 Hewett Road
Wyncote, PA 19095
Firm POC, Principal Investigator


The Formula Factory 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 approach that will be used allows the use of traditional forms of program reasoning using assertions about the global state, achieving soundness for weak memory by introducing additional proof obligations and constraints on the use of ghost data. This will allow the proven verification methodology to be reused.