From 7109ef607ebb1b56dfcc62165f59508af6779f44 Mon Sep 17 00:00:00 2001
From: pmaksimo <p.maksimovic@imperial.ac.uk>
Date: Wed, 13 May 2020 19:16:29 +0100
Subject: [PATCH] minor corrections
---
publications.bib | 94 ++++++++++++++++++++++++------------------------
1 file changed, 47 insertions(+), 47 deletions(-)
diff --git a/publications.bib b/publications.bib
index 14a24b9..add2a19 100644
--- a/publications.bib
+++ b/publications.bib
@@ -1756,26 +1756,26 @@ school = {Imperial College London},
year = {2020},
type = {phdthesis},
project = {concurrency},
-abstract = {The cloud has become popular for its low cost, high availability and
-high fault-tolerance-queue or de-queue, for example Amazon Web Service (AWS) and
-Google Cloud Platform (GCP. Those cloud infrastructures provide fixed interface,
-to hide the complex internal implementation that consists of hundreds of thousands
-of machines globally that work together as a whole system, known as a distributed
-system. Clients of those systems only need to work with the abstract interfaces.
-Transactions are the de facto interfaces in modern distributed databases.
-Because of the CAP theorem, a distributed system must sacrifice strong consistency
-to achieve high availability and high fault-tolerance. Engineers and researchers
-have proposed many reference implementations in specific setting for various weak
-consistency models. However, there have been little work on formalising the interfaces.
-We introduce an interleaving operational semantics for describing such interfaces,
-with the focus on the client-observable behaviour of atomic transactions on
-distributed key-value stores. Our semantics builds on abstract states comprising
-centralised, global key-value stores and partial client views. We provide
-operational definitions of consistency models for our key-value stores which
-are shown to be equivalent to the well-known declarative definitions of consistency
-models for execution graphs. We explore two immediate applications of our semantics:
-specific protocols of databases for a specific consistency can be verified in
-our centralised semantics; programs can be directly shown to have invariant
+abstract = {The cloud has become popular for its low cost, high availability and
+high fault-tolerance-queue or de-queue, for example Amazon Web Service (AWS) and
+Google Cloud Platform (GCP. Those cloud infrastructures provide fixed interface,
+to hide the complex internal implementation that consists of hundreds of thousands
+of machines globally that work together as a whole system, known as a distributed
+system. Clients of those systems only need to work with the abstract interfaces.
+Transactions are the de facto interfaces in modern distributed databases.
+Because of the CAP theorem, a distributed system must sacrifice strong consistency
+to achieve high availability and high fault-tolerance. Engineers and researchers
+have proposed many reference implementations in specific setting for various weak
+consistency models. However, there have been little work on formalising the interfaces.
+We introduce an interleaving operational semantics for describing such interfaces,
+with the focus on the client-observable behaviour of atomic transactions on
+distributed key-value stores. Our semantics builds on abstract states comprising
+centralised, global key-value stores and partial client views. We provide
+operational definitions of consistency models for our key-value stores which
+are shown to be equivalent to the well-known declarative definitions of consistency
+models for execution graphs. We explore two immediate applications of our semantics:
+specific protocols of databases for a specific consistency can be verified in
+our centralised semantics; programs can be directly shown to have invariant
properties such as robustness results against a weak consistency model.},
}
@@ -1788,40 +1788,40 @@ title = {Data Consistency in Transactional Storage Systems: a Centralised Ap
booktitle = {34th European Conference on Object-Oriented Programming (ECOOP 2020)},
project = {concurrency},
year = {2020},
-abstract = {We introduce an interleaving operational semantics for describing the
-client-observable behaviour of atomic transactions on distributed key-value stores.
-Our semantics builds on abstract states comprising centralised, global key-value
-stores and partial client views. We provide operational definitions of consistency
-models for our abstract states which we show to be equivalent to the well known
-declarative definitions of consistency model on abstract executions. We explore
-two applications, verifying that the COPS replicated database and the Clock-SI
-partitioned database satisfy their consistency models using trace refinement,
+abstract = {We introduce an interleaving operational semantics for describing the
+client-observable behaviour of atomic transactions on distributed key-value stores.
+Our semantics builds on abstract states comprising centralised, global key-value
+stores and partial client views. We provide operational definitions of consistency
+models for our abstract states which we show to be equivalent to the well known
+declarative definitions of consistency model on abstract executions. We explore
+two applications, verifying that the COPS replicated database and the Clock-SI
+partitioned database satisfy their consistency models using trace refinement,
and proving invariant properties of client programs.},
}
@InProceedings{Sampaio2020Trusted,
-author = {Gabriela Sampaio and
- Jos{\'{e}} {Fragoso Santos} and
- Petar Maksimovi\'{c}
- and Philippa Gardner},
+author = {Gabriela Sampaio and
+ Jos{\'{e}} {Fragoso Santos} and
+ Petar Maksimovi\'{c}
+ and Philippa Gardner},
title = {A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications},
booktitle = {34th European Conference on Object-Oriented Programming (ECOOP 2020)},
-project = { gillian },
+project = { web },
year = {2020},
-abstract = {We introduce a trusted infrastructure for symbolic analysis of modern
-event-driven Web applications. This infrastructure consists of reference
-implementations of the DOM Core Level 1 and UI Events, JavaScript Promises,
-and the JavaScript async/await APIs, all underpinned by a simple Core Event
-Semantics that is sufficiently expressive to describe the event models underlying
-all these APIs. Our reference implementations are trustworthy in that they follow
-the API respective standards line-by-line and they are thoroughly tested against
-the appropriate official test-suites, passing all the applicable tests. Using the
-Core Events Semantics and the reference implementations, we develop JaVerT.Click,
-a symbolic execution tool for JavaScript that, for the first time, supports reasoning
-about JavaScript programs that use some (possibly all) these APIs. Using JaVerT.Click,
-we perform comprehensive symbolic testing of the events module of Cash, a widely-used jQuery
-alternative, creating a symbolic test suite with 100 per cent line coverage, establishing bounded
-correctness of several essential properties of the module, and discovering two subtle,
+abstract = {We introduce a trusted infrastructure for symbolic analysis of modern
+event-driven Web applications. This infrastructure consists of reference
+implementations of the DOM Core Level 1 and UI Events, JavaScript Promises,
+and the JavaScript async/await APIs, all underpinned by a simple Core Event
+Semantics that is sufficiently expressive to describe the event models underlying
+all these APIs. Our reference implementations are trustworthy in that they follow
+the API respective standards line-by-line and they are thoroughly tested against
+the appropriate official test-suites, passing all the applicable tests. Using the
+Core Events Semantics and the reference implementations, we develop JaVerT.Click,
+a symbolic execution tool for JavaScript that, for the first time, supports reasoning
+about JavaScript programs that use some (possibly all) these APIs. Using JaVerT.Click,
+we perform comprehensive symbolic testing of the events module of Cash, a widely-used jQuery
+alternative, creating a symbolic test suite with 100 per cent line coverage, establishing bounded
+correctness of several essential properties of the module, and discovering two subtle,
previously unknown bugs.},
}
--
GitLab