You are here

A Verifier for Multicore C11 or C++11 Code

Award Information
Agency: Department of Commerce
Branch: National Institute of Standards and Technology
Contract: 70NANB15H298N
Agency Tracking Number: 058.03.01-2015
Amount: $99,909.92
Phase: Phase I
Program: SBIR
Solicitation Topic Code: 9.03.01.77-R
Solicitation Number: N/A
Timeline
Solicitation Year: 2015
Award Year: 2015
Award Start Date (Proposal Award Date): 2015-09-01
Award End Date (Contract End Date): 2016-02-19
Small Business Information
421 SW Sixth Ave., Suite 300, Portland, OR, 97204
DUNS: 098009918
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Joe Kiniry
 (503) 808-7183
 kiniry@galois.com
Business Contact
 Joe Kiniry
Phone: (503) 808-7183
Email: kiniry@galois.com
Research Institution
N/A
Abstract
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.

* Information listed above is at the time of submission. *

US Flag An Official Website of the United States Government