Add more content

1 files changed, 25 insertions, 0 deletions

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"
+}