From c258a14a48bf5cc7ffe22f26edf03f55a92573d2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 15 Nov 2020 18:17:36 +0000 Subject: Add more content --- references.bib | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'references.bib') diff --git a/references.bib b/references.bib index 6e2babd..cd232b5 100644 --- a/references.bib +++ b/references.bib @@ -503,3 +503,28 @@ publisher = {Association for Computing Machinery}, series = {PLDI '11} } + +@inproceedings{blazy05_formal_verif_memor_model_c, + author = "Blazy, Sandrine and Leroy, Xavier", + title = "Formal Verification of a Memory Model for C-Like Imperative + Languages", + tags = {verification}, + booktitle = "Formal Methods and Software Engineering", + year = 2005, + pages = "280--299", + abstract = "This paper presents a formal verification with the Coq proof + assistant of a memory model for C-like imperative + languages. This model defines the memory layout and the + operations that manage the memory. The model has been + specified at two levels of abstraction and implemented as part + of an ongoing certification in Coq of a moderately-optimising + C compiler. Many properties of the memory have been verified + in the specification. They facilitate the definition of + precise formal semantics of C pointers. A certified OCaml code + implementing the memory model has been automatically extracted + from the specifications.", + address = "Berlin, Heidelberg", + editor = "Lau, Kung-Kiu and Banach, Richard", + isbn = "978-3-540-32250-4", + publisher = "Springer Berlin Heidelberg" +} -- cgit