enter search term and/or author name
MCALIB: Measuring Sensitivity to Rounding Error with Monte Carlo Programming
Michael Frechtling, Philip H. W. Leong
Article No.: 5
Runtime analysis provides an effective method for measuring the sensitivity of programs to rounding errors. To date, implementations have required significant changes to source code, detracting from their widespread application. In this work, we...
A fully abstract compiler prevents security features of the source language from being bypassed by an attacker operating at the target language level. Unfortunately, developing fully abstract compilers is very complex, and it is even more so when...
Verification of a Cryptographic Primitive: SHA-256
Andrew W. Appel
Article No.: 7
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....