A formal C memory model supporting integer-pointer casts.

Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis

Browse the full PLDI paper archive.