Update publications.bib

publications.bib

@@ -1587,6 +1587,28 @@ exhibit the desired behaviour.},
   doi           = {https://doi.org/10.1016/j.jlamp.2018.03.003},
   keywords      = {Concurrency, Specification, Program verification},
   url           = {http://www.sciencedirect.com/science/article/pii/S2352220817300871},
+  
+ @InProceedings{Ntzik2018Concurrent,
+  author    = {Gian Ntzik and Pedro da Rocha Pinto and Julian Sutherland  and Philipa Gardner},
+  title     = {A Concurrent Specification of POSIX File Systems },
+  booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018).},
+  year      = {2018},
+  month     = jul,
+  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 specification 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 the example of lock files.},
+file      = {:Ntzik2018Concurrent.pdf:PDF},
+
 
 }