Commit 07d70bf3 authored by Petar Maksimovic's avatar Petar Maksimovic
Browse files

ESL correction

parent 22a57de4
......@@ -1648,7 +1648,7 @@ in JavaScript verification; and the feasibility of automatic compositional testi
@InProceedings{Bodin2019Skeletal,
author = {Martin Bodin and Philippa Gardner and Thomas Jensen and Alan Schmitt},
title = {Skeletal Semantics and their Interpretations},
booktitle = {Proceedings of the 46\textsuperscript{th} {ACM} {SIGPLAN-SIGACT}
booktitle = {Proceedings of the 46\textsuperscript{th} {ACM} {SIGPLAN-SIGACT}
Symposium on Principles of Programming Languages (POPL'19)},
volume = {3},
number = {{POPL}},
......@@ -1862,12 +1862,12 @@ title = {TaDA Live: Compositional Reasoning for Termination of Fine-grained
Concurrent Programs},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021.},
year = {2021},
publisher = {Association for Computing Machinery},
volume = {43},
number = {4},
issn = {0164-0925},
url = {https://doi.org/10.1145/3477082},
doi = {10.1145/3477082},
publisher = {Association for Computing Machinery},
volume = {43},
number = {4},
issn = {0164-0925},
url = {https://doi.org/10.1145/3477082},
doi = {10.1145/3477082},
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,
......@@ -1910,9 +1910,9 @@ two bugs in the JavaScript and three bugs in the C implementation.},
@InProceedings{Watt2021Two,
author = {Conrad Watt and
Xiaojia Rao and
Xiaojia Rao and
Jean Pichon-Pharabod and
Martin Bodin and
Martin Bodin and
Philippa Gardner},
title = {Two Mechanisations of WebAssembly 1.0},
booktitle = {Proceedings of the 24\textsuperscript{th} international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021},
......@@ -1928,28 +1928,28 @@ url = {https://doi.org/10.1007/978-3-030-90870-6\_4},
doi = {10.1007/978-3-030-90870-6\_4},
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
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.
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
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.
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.
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.
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
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
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.},
}
@InProceedings{MaksimovicExact2022,
@InProceedings{Maksimovic2022Exact,
author = {Petar Maksimoví\'c and
Caroline Cronj\"ager and
Julian Sutherland and
......
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