Sciweavers

Share
PLDI
2015
ACM

A formal C memory model supporting integer-pointer casts

4 years 12 months ago
A formal C memory model supporting integer-pointer casts
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 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. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.2.4 [Software Engineering]: Software/Program Verification Keywords...
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitr
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where PLDI
Authors Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
Comments (0)
books