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...
Autor principal: | |
---|---|
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 |