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

Update publications.bib

parent d588644a
......@@ -1825,16 +1825,16 @@ previously unknown bugs.},
}
@Article{DOsualdo2020TaDa,
author = {Emanuele D'Osualdo and
Azadeh Farzan and
Philippa Gardner and
Julian Sutherland},
title = {TaDA Live: Compositional Reasoning for Termination of Fine-grained
Concurrent Programs},
journal = {CoRR},
volume = {abs/1901.05750},
year = {2020},
abstract = {We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of
author = {Emanuele D'Osualdo and
Azadeh Farzan and
Philippa Gardner and
Julian Sutherland},
title = {TaDA Live: Compositional Reasoning for Termination of Fine-grained
Concurrent Programs},
journal = {CoRR},
volume = {abs/1901.05750},
year = {2020},
abstract = {We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of
blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking:
that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in,
for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications
......@@ -1873,23 +1873,23 @@ 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},
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}
@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,
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
......@@ -1900,6 +1900,39 @@ designing common abstractions used for both verification tasks, and find
two bugs in the JavaScript and three bugs in the C implementation.},
}
@InProceedings{Watt2021Two,
author = {Conrad Watt and
Xiaojia Rao and
Jean Pichon-Pharabod and
Martin Bodin and
Philippa Gardner},
title = {Two mechanisations of WebAssembly 1.0},
booktitle = {Proceedings of the 24th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021},
year = {2021},
abstract = {WebAssembly (Wasm) is a new bytecode language supported
by all major Web browsers, designed primarily to be an efficient compilation
target for low-level languages such as C/C++ and Rust. It is unusual in that
it is officially specified through a formal semantics. An initial draft
specification was published in 2017 with an associated mechanised
specification in Isabelle/HOL published by Watt that found
bugs in the original specification, fixed before its publication.
The first official W3C standard, WebAssembly 1.0, was published in
2019. Building on Watt's original mechanisation, we introduce two
mechanised specifications of the WebAssembly 1.0 semantics, written
in different theorem provers: WasmCert-Isabelle and WasmCert-Coq.
Wasm's compact design and official formal semantics enable our mechanisations
to be particularly complete and close to the published language standard.
We present a high-level description of the language's updated
type soundness result, referencing both mechanisations.
We also describe the current state of the mechanisation of language features not previously
supported: WasmCert-Isabelle includes a verified executable definition
of the instantiation phase as part of an executable verified interpreter;
WasmCert-Coq includes executable parsing and numeric definitions as
on-going work towards a more ambitious end-to-end verified interpreter
which does not require an OCaml harness like WasmCert-Isabelle.},
}
@Comment{jabref-meta: databaseType:bibtex;}
@Comment{jabref-meta: saveActions:enabled;
......
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