To refer to this page use:
http://arks.princeton.edu/ark:/88435/pr19p42| Abstract: | This article presents 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 with respect to the operational semantics for C, connected to the CompCert verified optimizing C compiler. |
| Publication Date: | 16-Apr-2015 |
| Citation: | Appel, Andrew W. "Verification of a Cryptographic Primitive" ACM Transactions on Programming Languages and Systems, (2), 37, 1 - 31, doi:10.1145/2701415 |
| DOI: | doi:10.1145/2701415 |
| ISSN: | 0164-0925 |
| Pages: | 1 - 31 |
| Type of Material: | Journal Article |
| Journal/Proceeding Title: | ACM Transactions on Programming Languages and Systems |
| Version: | This is the author’s final manuscript. All rights reserved to author(s). |
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.