This article presents a full formal machine-checked verification of a C program: theOpenSSL implementation of SHA-256. This is an interactive proof of functional correctness in the Coq proof assistant, using the Verifiable C program logic. Verifiable C is a separation logic for the C language, proved sound with respect to the operational semantics for C, connected to the CompCert verified optimizing C compiler.
|Original language||English (US)|
|Journal||ACM Transactions on Programming Languages and Systems|
|State||Published - Apr 1 2015|
All Science Journal Classification (ASJC) codes