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

The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications.

We present the first formal memory model that allows many common optimizations and “fully” supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq.

PLDI 2015 Artifact Evaluated Badge

Conference Day
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 KangSeoul National University, Chung-Kil HurSeoul National University, William ManskyUniversity of Pennsylvania, Dmitri GarbuzovUniversity of Pennsylvania, Steve Zdancewic, Viktor VafeiadisMPI-SWS, Germany
Media Attached
14:25
25m
Talk
Defining the undefinedness of C
Research Papers
Chris HathhornUniversity of Missouri, Chucky EllisonUniversity of Illinois, Grigore RoşuUniversity of Illinois at Urbana-Champaign
Media Attached
14:50
25m
Talk
KJS: A Complete Formal Semantics of JavaScript
Research Papers
Daejun ParkUniversity of Illinois at Urbana-Champaign, Andrei StefanescuUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
Media Attached
15:15
25m
Talk
Verdi: A Framework for Formally Verifying Distributed System Implementations
Research Papers
James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington, Pavel PanchekhaUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Xi WangUniversity of Washington, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of Washington
Media Attached