From 5adac34105258c3beba622ad6ea49b21e439fb63 Mon Sep 17 00:00:00 2001
From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk>
Date: Mon, 30 Aug 2021 11:13:37 +0000
Subject: [PATCH] Update publications.bib
---
publications.bib | 34 +++++++++++++++++++++++++---------
1 file changed, 25 insertions(+), 9 deletions(-)
diff --git a/publications.bib b/publications.bib
index eb7b52e..236729c 100644
--- a/publications.bib
+++ b/publications.bib
@@ -1860,15 +1860,31 @@ certificate of correctness. We provide a prototype implementation and we report
on some textbook examples.},
}
-@InProceedings{Maksimovic2021Gillian,
-author = {Petar Maksimovic and
- Sacha{-}{\'{E}}lie Ayoun and
- Jos{\'{e}} Fragoso Santos and
- Philippa Gardner},
- title ={{Gillian, Part II: Real-World Verification for
-JavaScript and C}},
-booktitle = {33rd International Conference on Computer-Aided Verification, (CAV 2021)},
-year = {2021},
+ @inproceedings{Maksimovic2021Gillian,
+ author = {Petar Maksimovic and
+ Sacha{-}{\'{E}}lie Ayoun and
+ Jos{\'{e}} Fragoso Santos and
+ Philippa Gardner},
+ editor = {Alexandra Silva and
+ K. Rustan M. Leino},
+ title = {Gillian, Part {II:} Real-World Verification for JavaScript and {C}},
+ booktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
+ 2021, Virtual Event, July 20-23, 2021, Proceedings, Part {II}},
+ series = {Lecture Notes in Computer Science},
+ volume = {12760},
+ pages = {827--850},
+ publisher = {Springer},
+ year = {2021},
+ doi = {10.1007/978-3-030-81688-9\_38},
+ abstract = {We introduce verification based on separation logic to Gillian,
+a multi-language platform for the development of symbolic analysis tools
+which is parametric on the memory model of the target language. Our
+work develops a methodology for constructing compositional memory
+models for Gillian, leading to a unified presentation of the JavaScript and
+C memory models. We verify the JavaScript and C implementations of the
+AWS Encryption SDK message header deserialisation module, specifically
+designing common abstractions used for both verification tasks, and find
+two bugs in the JavaScript and three bugs in the C implementation.},
}
@Comment{jabref-meta: databaseType:bibtex;}
--
GitLab