@@ -576,6 +576,14 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
...
@@ -576,6 +576,14 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
abstract={In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the sequence of steps that needs to be taken. We briefly describe \javert, our semi-automatic toolchain for JavaScript verification.},
abstract={In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the sequence of steps that needs to be taken. We briefly describe \javert, our semi-automatic toolchain for JavaScript verification.},
project={web},
project={web},
}
}
@InProceedings{Cerone2017Algebraic,
author={Andrea Cerone and Alexey Gotsman and Hongseok Yang},
title={Algebraic Laws for Weak Consistency},
booktitle={Proceedings of 28\textsuperscript{th} International Conference on Concurrency Theory, (Concur 2017)}},
year = {2017},
abstract = {Modern distributed systems often rely on so called weakly-consistent databases, which achieve scalability by sacrificing the consistency guarantee of distributed transaction processing. Such databases have been formalised in two different styles, one based on abstract executions and the other based on dependency graphs. The choice between these styles has been made according to intended applications. The former has been used for specifying and verifying the implementation of these databases, while the latter for proving properties of client programs of the databases. In this paper, we present a set of novel algebraic laws (i.e. inequations) that connect these two styles of specifications. The laws relate binary relations used in a specification based on abstract executions, to those used in a specification based on dependency graphs. We then show that this algebraic connection gives rise to so called robustness criteria, conditions which ensure that a client program of a weakly-consistent database does not exhibit anomalous behaviours due to weak consistency. These criteria make it easy to reason about these client programs, and may become a basis for dynamic or static program analyses. For a certain class of consistency models specifications, we prove a full abstraction result that connects the two styles of specifications.},
