@inproceedings{1f880543a7bd4036902d48d8b411acc8,
title = "Verification of a cryptographic primitive: SHA-256 (abstract)",
abstract = "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.",
keywords = "COQ",
author = "Appel, {Andrew W.}",
note = "Publisher Copyright: {\textcopyright} 2015 ACM.; 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 ; Conference date: 13-06-2015 Through 17-06-2015",
year = "2015",
month = jun,
day = "3",
doi = "10.1145/2737924.2774972",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "153",
editor = "Steve Blackburn and David Grove",
booktitle = "PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation",
}