Tue 16 Jun 2015 14:25 - 14:50 at PLDI Main RED (Portland 256) - Semantics I Chair(s): Hans-J. Boehm

We present a ``negative'' semantics of the C11 language—a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it. We have used these techniques to modify and extend a semantics of C into one that captures undefined behavior. The amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end nearly doubling the size of the original semantics. From our semantics, we have automatically extracted an undefinedness checker, which we evaluate against other popular analysis tools, using our own test suite in addition to a third-party test suite. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself.

Tue 16 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:40
14:00
25m
Talk
A Formal C Memory Model Supporting Integer-Pointer Casts
Research Papers
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, William Mansky University of Pennsylvania, Dmitri Garbuzov University of Pennsylvania, Steve Zdancewic , Viktor Vafeiadis MPI-SWS, Germany
Media Attached
14:25
25m
Talk
Defining the undefinedness of C
Research Papers
Chris Hathhorn University of Missouri, Chucky Ellison University of Illinois, Grigore Roşu University of Illinois at Urbana-Champaign
Media Attached
14:50
25m
Talk
KJS: A Complete Formal Semantics of JavaScript
Research Papers
Daejun Park University of Illinois at Urbana-Champaign, Andrei Stefanescu University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
Media Attached
15:15
25m
Talk
Verdi: A Framework for Formally Verifying Distributed System Implementations
Research Papers
James R. Wilcox University of Washington, Doug Woos University of Washington, Pavel Panchekha University of Washington, Zachary Tatlock University of Washington, Seattle, Xi Wang University of Washington, Michael D. Ernst University of Washington, Thomas Anderson University of Washington
Media Attached