diff --git a/publications.bib b/publications.bib
index 8bf34f7b05269b6e05a6722b411fbc681c498141..e9ab7e1e301b83310cf50bb454287e95840ae567 100644
--- a/publications.bib
+++ b/publications.bib
@@ -427,7 +427,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
Author = {Gian Ntzik and Philippa Gardner},
Booktitle = {Proceedings of the 30\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
Year = {2015},
- Note = {(Awaiting Publication)},
+ Month = {October},
Abstract = {We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including ?..? and symbolic links) which may overlap the directories be- ing updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no ?..? or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.}
}
@@ -437,7 +437,8 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
Author = {Gian Ntzik and Pedro {da Rocha Pinto} and Philippa Gardner},
Booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
Year = {2015},
- Note = {(Awaiting Publication)$^*$},
+ Month = {December},
+ Pages = {169--188},
Abstract = {Separation logic has been successful at verifying that pro- grams do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.}
}
@@ -488,6 +489,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Mark J. Wheelhouse},
Booktitle = {Proceedings of the 26\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
Year = {2011},
+ Month = {October},
Pages = {845--864},
Abstract = {Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is in- sufficient for reasoning about indexes that are accessed con- currently.
@@ -499,6 +501,7 @@ We present an abstract specification for concurrent indexes. We verify several r
Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale{-}Young and Philippa Gardner},
Booktitle = {Proceedings of the 28\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
Year = {2014},
+ Month = {July},
Pages = {207--231},
Abstract = {To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concur- rent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.
@@ -510,6 +513,8 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner},
Booktitle = {Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics},
Year = {2015},
+ Month = {June},
+ Pages = {3--18},
Abstract = {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.}
}
@@ -519,6 +524,8 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner and Julian Sutherland},
Booktitle = {Proceedings of the 25\textsuperscript{th} European Symposium on Programming ({ESOP})},
Year = {2016},
+ Month = {April},
+ Pages = {207--231},
Abstract = {We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. 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 non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.}
}