Types, bytes, and separation logic

Symposium on Principles of Programming Languages, pp. 97-108, 2007.

Cited by: 197|Views20
EI

Abstract:

We present a formal model of memory that both captures the low- level features of C's pointers and memory, and that forms the basis for an expressive implementation of separation logic. At the low level, we do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap. At the level...More

Code:

Data:

Your rating :
0

 

Tags
Comments