Programming Languages and Systems (TOPLAS)


Search Issue
enter search term and/or author name


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 37 Issue 2, April 2015

MCALIB: Measuring Sensitivity to Rounding Error with Monte Carlo Programming
Michael Frechtling, Philip H. W. Leong
Article No.: 5
DOI: 10.1145/2665073

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...

Secure Compilation to Protected Module Architectures
Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, Frank Piessens
Article No.: 6
DOI: 10.1145/2699503

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
DOI: 10.1145/2701415

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....