Mon 15 Jun 2015 17:15 - 17:40 at PLDI Main RED (Portland 256) - TOPLAS Chair(s): Michelle Strout

A full formal machine-checked verification of a C program: the OpenSSL 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 w.r.t. the operational semantics for C, connected to the CompCert verified optimizing C compiler.

Published in ACM Transactions on Programming Languages and Systems 37(2) 7:1-7:31, March 2015

Mon 15 Jun

17:15 - 17:40: Research Papers - TOPLAS at PLDI Main RED (Portland 256)
Chair(s): Michelle StroutColorado State University
pldi2015-papers17:15 - 17:40
Andrew AppelPrinceton