Updated keys.

index.md

@@ -11,7 +11,7 @@ We have to take shared state that is being changed by multiple threads into acco
 
 Our research agenda is to develop formal reasoning methods about concurrency with a focus on concurrent program logics.
 Recently, there have been various logics based on separation logic to verify functional correctness of fine-grained concurrent programs.
-We have played a significant role introducing {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, the {% cite_details Dinsdale-Young2013Views --text Views framework %}, {% cite_details RochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details RochaPinto2016Modular --text Total-TaDA %}.
+We have played a significant role introducing {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, the {% cite_details Dinsdale-Young2013Views --text Views framework %}, {% cite_details daRochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details daRochaPinto2016Modular --text Total-TaDA %}.
 These logics have tackled a range of problems, ranging data abstraction, atomicity abstraction, fault-tolerance, terminal, as well as introducing more modular and compositional ways to reason about concurrent programs.
 We have applied these logics to verify large problems, such as data structures used in databases and java.util.concurrent, as well as specifying file systems.
 

publications.bib

@@ -484,7 +484,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
   Abstract                 = {We present a separation logic framework which can express proper- ties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.}
 }
 
-@InProceedings{RochaPinto2011Simple,
+@InProceedings{daRochaPinto2011Simple,
   Title                    = {{A Simple Abstraction for Complex Concurrent Indexes}},
   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})},
@@ -496,7 +496,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
 We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, how- ever, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and BLink trees. The complexity of these algorithms, in particular the BLink tree algorithm, can be completely hidden from the client?s view by our abstract specification.}
 }
 
-@InProceedings{RochaPinto2014TaDA,
+@InProceedings{daRochaPinto2014TaDA,
   Title                    = {{TaDA: A Logic for Time and Data Abstraction}},
   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})},
@@ -508,7 +508,7 @@ We present an abstract specification for concurrent indexes. We verify several r
 Building on separation logic with concurrent abstract predicates (CAP), we introduce TaDA, a program logic which combines the benefits of abstract atomicity and abstract disjointness. We give several examples: an atomic lock module, a CAP example with a twist, which cannot be done using linearisability; an atomic MCAS module implemented using our lock module, a classic linearisability example which cannot be done us- ing CAP; and a double-ended queue module implemented using MCAS.}
 }
 
-@InProceedings{RochaPinto2015Steps,
+@InProceedings{daRochaPinto2015Steps,
   Title                    = {{Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)}},
   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},
@@ -519,7 +519,7 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
   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.}
 }
 
-@InProceedings{RochaPinto2016Modular,
+@InProceedings{daRochaPinto2016Modular,
   Title                    = {Modular Termination Verification for Non-blocking Concurrency},
   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})},