Commit 5adac341 authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia
Browse files

Update publications.bib

parent aefaf62f
......@@ -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;}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment