no more conflicts

README.md

@@ -8,7 +8,8 @@ references, and associated materials.
 1. To fulfill funding and REF requirements and for long-term archival, all papers and
    tech reports should be deposited into
    [Imperial Spiral](http://spiral.imperial.ac.uk/) within THREE MONTHS OF ACCEPTANCE. Do this now, so you don't
-   forget and email Teresa with a copy of the accepted submission so that she can add it on the news section of the website.
+   forget. Once this is done, email Teresa with a copy of the accepted submission so that she can publish the details of 
+the acceptance in the news section of the website.
 
 2. Create a BibTeX record for the publication in
    the [publications.bib](publications.bib) file. Post-publication, records can
@@ -39,6 +40,8 @@ Fields:
 * **url**: This field should **not** contain a duplicate of the doi. It
   generally only used to link to the publisher's version if the publisher does
   not also issue a DOI.
+* **month**: Add the exact date of the conference as publication date. 
+  This will keep the file hidden until the actual publication date.
 * **file**: This field is added automatically by the JabRef reference manager,
   it is ignored by the website. It is mostly useful as a quick check in the
   JabRef user interface that all publications have an associated file. See next

publications.bib

@@ -93,6 +93,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   title     = {Reasoning About POSIX File Systems},
   school    = {Imperial College London},
   year      = {2017},
+  month     = may,
   type      = {phdthesis},
   abstract  = {POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard's description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our speciation is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to lock files and named pipes. Program reasoning based on separation logic has been successful at verifying that programs do not crash due to illegal use of resources, such invalid memory accesses. The underlying assumption of separation logics, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, such as power loss, corrupting resources or resulting in permanent data loss. Critical software, such as file systems and databases, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about programs in the presence of such events and their associated recovery methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, such a stylised ARIES recovery algorithm.},
   file      = {Ntzik2017Reasoning.pdf:Ntzik2017Reasoning.pdf:PDF},
@@ -105,6 +106,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   title     = {Reasoning with Time and Data Abstractions},
   school    = {Imperial College London},
   year      = {2017},
+  month     = may,
   type      = {phdthesis},
   abstract  = {In this thesis, we address the problem of verifying the functional correctness of concurrent programs, with emphasis on fine-grained concurrent data structures. Reasoning about such programs is challenging since data can be concurrently accessed by multiple threads: the reasoning must account for the interference between threads, which is often subtle. To reason about interference, concurrent operations should either be at distinct times or on distinct data. We present TaDA, a sound program logic for verifying clients and implementations that use abstract specifications that incorporate both abstract atomicity—the abstraction that operations take effect at a single, discrete instant in time—and abstract disjointness—the abstraction that operations act on distinct data resources. Our key contribution is the introduction of atomic triples, which offer an expressive approach for specifying program modules. We also present Total-TaDA, a sound extension of TaDA with which we can verify total correctness of concurrent programs, i.e. that such programs both produce the correct result and terminate. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for nonblocking algorithms and express lock- and wait-freedom. More generally, the abstract specifications can express that one operation cannot impede the progress of another, a new non-blocking property that we call non-impedance. Finally, we describe how to extend TaDA for proving abstract atomicity for data structures that make use of helping—where one thread is performing an abstract operation on behalf of another—and speculation—where an abstract operation is determined by future behaviour.},
   file      = {daRochaPinto2017Reasoning.pdf:daRochaPinto2017Reasoning.pdf:PDF},
@@ -117,6 +119,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   title     = {Abstraction, Refinement and Concurrent Reasoning},
   school    = {Imperial College London},
   year      = {2017},
+  month     = jun,
   type      = {phdthesis},
   abstract  = {This thesis explores the challenges in abstract library specification, library refinement and reasoning about fine-grained concurrent programs.For abstract library specification, this thesis applies structural separation logic (SSL) to formally specify the behaviour of several libraries in an abstract, local and compositional manner. This thesis further generalises the theory of SSL to allow for library specifications that are language independent. Most notably, we specify a fragment of the Document Object Model (DOM) library. This result is compelling as it significantly improves upon existing DOM formalisms in that the specifications produced are local, compositional and language-independent. Concerning library refinement, this thesis explores two existing approaches to library refinement for separation logic, identifying their advantages and limitations in different settings. This thesis then introduces a hybrid approach to refinement, combining the strengths of both techniques for simple scalable library refinement. These ideas are then adapted to refinement for SSL by presenting a JavaScript implementation of the DOM fragment studied and establishing its correctness with respect to its specification using the hybrid refinement approach.As to concurrent reasoning, this thesis introduces concurrent local subjective logic (CoLoSL) for compositional reasoning about fine-grained concurrent programs. CoLoSL introduces subjective views, where each thread is verified with respect to a customised local view of the state, as well as the general composition and framing of interference relations, allowing for better proof reuse.},
   file      = {Raad2017Abstraction.pdf:Raad2017Abstraction.pdf:PDF},
@@ -124,6 +127,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   project   = { concurrency },
 }
 
+
 @InProceedings{FragosoSantos2017Towards,
   author    = {Jos{\'{e}} {Fragoso Santos} and Philippa Gardner and Petar Maksimovi\'{c} and Daiva Naud\v{z}i\={u}nien\.{e}},
   title     = {{Towards Logic-based Verification of JavaScript Programs}},
@@ -137,6 +141,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
   url       = {https://link.springer.com/chapter/10.1007/978-3-319-63046-5_2},
 }
 
+
 @InProceedings{Cerone2017Algebraic,
   author    = {Andrea Cerone and Alexey Gotsman and Hongseok Yang},
   title     = {Algebraic Laws for Weak Consistency},
@@ -1268,6 +1273,24 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
   project   = { concurrency, tada },
 }
 
+@proceedings{DBLP:conf/concur/2004,
+  editor    = {Philippa Gardner and
+               Nobuko Yoshida},
+  title     = {{CONCUR} 2004 - Concurrency Theory, 15th International Conference,
+               London, UK, August 31 - September 3, 2004, Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {3170},
+  publisher = {Springer},
+  year      = {2004},
+  url       = {https://doi.org/10.1007/b100113},
+  doi       = {10.1007/b100113},
+  isbn      = {3-540-22940-X},
+  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/concur/2004},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+
 @Comment{jabref-meta: databaseType:bibtex;}
 
 @Comment{jabref-meta: saveActions:enabled;