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

Update publications.bib

parent 08297755
......@@ -1824,13 +1824,26 @@ correctness of several essential properties of the module, and discovering two s
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},
year = {2020},
@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 = {2019},
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
that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that
can reason about the termination of clients which use such operations without breaking their abstraction
boundaries, and the correctness of the implementations of the operations with respect to their abstract
specifications. We introduce a novel semantic model using layered subjective obligations to express liveness
invariants, and a proof system that is sound with respect to the model. The subtlety of our specifications and
reasoning is illustrated using several case studies.},
}
@InProceedings{DOsualdo2020Decidable,
author = {Emanuele D'Osualdo and
......@@ -1885,6 +1898,12 @@ 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