Cargando…

A Formal C Memory Model for Separation Logic

The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions...

Descripción completa

Detalles Bibliográficos
Autor principal: Krebbers, Robbert
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2016
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109957/
https://www.ncbi.nlm.nih.gov/pubmed/30174361
http://dx.doi.org/10.1007/s10817-016-9369-1