From fe75887a8858f82c71ca617c6d3f0c2db5af6cc2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 15 Nov 2020 20:12:52 +0000 Subject: More changes to Verilog section --- references.bib | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) (limited to 'references.bib') 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", +} -- cgit