More changes to Verilog section

1 files changed, 13 insertions, 11 deletions

diff --git a/references.bib b/references.bib
index cd232b5..29bd581 100644
--- a/references.bib
+++ b/references.bib
@@ -512,19 +512,21 @@
 	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"
 }
+
+@inproceedings{slind08_brief_overv_hol4,
+  author          = "Slind, Konrad and Norrish, Michael",
+  title           = "A Brief Overview of HOL4",
+  booktitle       = "Theorem Proving in Higher Order Logics",
+  year            = 2008,
+  pages           = "28--32",
+  address         = "Berlin, Heidelberg",
+  editor          = "Mohamed, Otmane Ait and Mu{\~{n}}oz, C{\'e}sar and Tahar, Sofi{\`e}ne",
+  isbn            = "978-3-540-71067-7",
+  keywords        = {theorem proving;HOL},
+  publisher       = "Springer Berlin Heidelberg",
+}