From 5ae83d5ed3809ab3d307485ff2abacec0009a798 Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Tue, 4 Apr 2017 16:20:27 +0100 Subject: [PATCH] Setting up jabref on Teresa's machine --- .gitignore | 2 ++ publications.bib | 21 ++++++++++----------- 2 files changed, 12 insertions(+), 11 deletions(-) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..50ad3d9 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +publications.bib.bak +publications.bib.sav diff --git a/publications.bib b/publications.bib index 13b895a..b790809 100644 --- a/publications.bib +++ b/publications.bib @@ -1,5 +1,4 @@ -% This file was created with JabRef 2.10. -% Encoding: UTF8 +% Encoding: UTF-8 @InProceedings{Bodin2014Trusted, @@ -548,15 +547,13 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro } @InProceedings{Xiong2017Abstract, - Title = {Abstract Specifications for Concurrent Maps}, - Author = {Shale Xiong and Pedro {da Rocha Pinto} and Gian Ntzik and Philippa Gardner}, - Booktitle = {Proceedings of the 26\textsuperscript{th} European Symposium on Programming ({ESOP})}, - Year = {2017}, - Month = {April}, - - Abstract = {Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.}, - - Project = { concurrency, tada } + author = {Shale Xiong and Pedro {da Rocha Pinto} and Gian Ntzik and Philippa Gardner}, + title = {Abstract Specifications for Concurrent Maps}, + booktitle = {Proceedings of the 26\textsuperscript{th} European Symposium on Programming ({ESOP})}, + year = {2017}, + month = {April}, + abstract = {Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.}, + project = {concurrency, tada}, } @Article{Fragoso2016Mashic, Title = {{Mashic Compiler: Mashup Sandboxing based on Inter-frame Communication}}, @@ -573,3 +570,5 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro Project = { web } } + +@Comment{jabref-meta: databaseType:bibtex;} -- GitLab