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.
Original language | English (US) |
---|---|
Title of host publication | PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation |
Publisher | Association for Computing Machinery |
Number of pages | 1 |
Volume | 2015-June |
ISBN (Electronic) | 9781450334686 |
DOIs | |
State | Published - Jun 3 2015 |
Event | 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 - Portland, United States Duration: Jun 13 2015 → Jun 17 2015 |
Other
Other | 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 |
---|---|
Country/Territory | United States |
City | Portland |
Period | 6/13/15 → 6/17/15 |
All Science Journal Classification (ASJC) codes
- Software