publications.bib 121 KB
Newer Older
1
% Encoding: UTF-8
Thomas Wood's avatar
Thomas Wood committed
2 3

@InProceedings{Bodin2014Trusted,
4 5 6 7 8 9 10
  author    = {Martin Bodin and Arthur Chargu{\'{e}}raud and Daniele Filaretti and Philippa Gardner and Sergio Maffeis and Daiva Naud\v{z}i\={u}nien\.{e} and Alan Schmitt and Gareth Smith},
  title     = {{A Trusted Mechanised {JavaScript} Specification}},
  booktitle = {Proceedings of the 41\textsuperscript{st} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'14})},
  year      = {2014},
  pages     = {87--100},
  abstract  = {JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.},
Thomas Wood's avatar
Thomas Wood committed
11
  doi       = {10.1145/2535838.2535876},
12 13
  file      = {Bodin2014Trusted.pdf:Bodin2014Trusted.pdf:PDF},
  project   = { web },
Thomas Wood's avatar
Thomas Wood committed
14 15
}

Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
16 17 18
@InProceedings{Raad2016DOM,
  author    = {Azalea Raad and Jos{\'{e}} {Fragoso Santos} and Philippa Gardner},
  title     = {{DOM:} Specification and Client Reasoning},
19
  booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems (APLAS'16)},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
  year      = {2016},
  pages     = {401--422},
  abstract  = {We present an axiomatic specification of a key fragment of DOM using structural separation logic. This specfication allows us to develop modular reasoning about client programs that call the DOM.},
  doi       = {10.1007/978-3-319-47958-3_21},
  file      = {Raad2016DOM.pdf:Raad2016DOM.pdf:PDF},
  project   = { web },
}

@InProceedings{Dinsdale-Young2017Caper,
  author    = {Thomas Dinsdale-Young and Pedro {da Rocha Pinto} and Kristoffer Just Andersen and Lars Birkedal},
  title     = {Caper: Automatic Verification for Fine-grained Concurrency},
  booktitle = {Proceedings of the 26\textsuperscript{th} European Symposium on Programming ({ESOP'17})},
  year      = {2017},
  pages     = {420--447},
  month     = apr,
  abstract  = {Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool for automated reasoning in such a logic. Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify the functional correctness of fine-grained concurrent algorithms.},
  doi       = {10.1007/978-3-662-54434-1_16},
  file      = {Dinsdale-Young2017Caper.pdf:Dinsdale-Young2017Caper.pdf:PDF;Dinsdale-Young2017Caper.techreport.pdf:Dinsdale-Young2017Caper.techreport.pdf:PDF},
Pedro da Rocha Pinto's avatar
Pedro da Rocha Pinto committed
38
  project   = { concurrency },
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
}

@Article{Luo2016Mashic,
  author   = {Zhengqin Luo and Jos{\'{e}} {Fragoso Santos} and Ana Almeida Matos and Tamara Rezk},
  title    = {{Mashic Compiler: Mashup Sandboxing based on Inter-frame Communication}},
  journal  = {Journal of Computer Security},
  year     = {2016},
  volume   = {1},
  number   = {24},
  pages    = {91--136},
  abstract = { Mashups are a prevailing kind of web applications integrating external gadget APIs often written in the JavaScript programming language. Writing secure mashups is a challenging task due to the heterogeneity of existing gadget APIs, the privileges granted to gadgets during mashup executions, and JavaScript’s highly dynamic environment. We propose a new compiler, called Mashic, for the automatic generation of secure JavaScript-based mashups from existing mashup code. The Mashic compiler can effortlessly be applied to existing mashups based on a wide-range of gadget APIs. It offers security and correctness guarantees. Security is achieved via the Same Origin Policy. Correctness is ensured in the presence of benign gadgets, that satisfy confidentiality and integrity constraints with regard to the integrator code. The compiler has been successfully applied to real world mashups based on Google maps, Bing maps, YouTube, and Zwibbler APIs.},
  doi      = {10.3233/JCS-160542},
  file     = {Luo2016Mashic.pdf:Luo2016Mashic.pdf:PDF},
  project  = { web },
}

@PhdThesis{Ntzik2017Reasoning,
  author    = {Gian Ntzik},
  title     = {Reasoning About POSIX File Systems},
  school    = {Imperial College London},
  year      = {2017},
  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},
  phdthesis = {Y},
Pedro da Rocha Pinto's avatar
Pedro da Rocha Pinto committed
64
  project   = { concurrency, tada },
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
65 66 67 68 69 70 71
}

@PhdThesis{daRochaPinto2017Reasoning,
  author    = {Pedro {da Rocha Pinto}},
  title     = {Reasoning with Time and Data Abstractions},
  school    = {Imperial College London},
  year      = {2017},
72
  month     = may,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
73 74 75 76
  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},
  phdthesis = {Y},
Pedro da Rocha Pinto's avatar
Pedro da Rocha Pinto committed
77
  project   = { concurrency, tada },
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
78 79 80 81 82 83 84
}

@PhdThesis{Raad2017Abstraction,
  author    = {Azalea Raad},
  title     = {Abstraction, Refinement and Concurrent Reasoning},
  school    = {Imperial College London},
  year      = {2017},
85
  month     = jun,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
86 87 88 89 90 91 92 93 94 95 96 97 98 99
  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},
  phdthesis = {Y},
  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}},
  booktitle = {Proceedings of 26\textsuperscript{th} Conference on Automated Deduction {(CADE 26)}},
  year      = {2017},
  month     = aug,
  abstract  = {In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the  sequence of steps that needs to be taken. We briefly describe \javert, our semi-automatic toolchain for JavaScript verification.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
100
  doi       = {10.1007/978-3-319-63046-5_2},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
101 102 103 104 105 106 107 108 109 110 111
  file      = {FragosoSantos2017Towards.pdf:FragosoSantos2017Towards.pdf:PDF},
  project   = {web},
}

@InProceedings{Cerone2017Algebraic,
  author    = {Andrea Cerone and Alexey Gotsman and Hongseok Yang},
  title     = {Algebraic Laws for Weak Consistency},
  booktitle = {Proceedings of 28\textsuperscript{th} International Conference on Concurrency Theory, (Concur 2017)},
  year      = {2017},
  month     = sep,
  abstract  = {Modern distributed systems often rely on so called weakly-consistent databases, which achieve scalability by sacrificing the consistency guarantee of distributed transaction processing. Such databases have been formalised in two different styles, one based on abstract executions and the other based on dependency graphs. The choice between these styles has been made according to intended applications. The former has been used for specifying and verifying the implementation of these databases, while the latter for proving properties of client programs of the databases. In this paper, we present a set of novel algebraic laws (i.e. inequations) that connect these two styles of specifications. The laws relate binary relations used in a specification based on abstract executions, to those used in a specification based on dependency graphs. We then show that this algebraic connection gives rise to so called robustness criteria, conditions which ensure that a client program of a weakly-consistent database does not exhibit anomalous behaviours due to weak consistency. These criteria make it easy to reason about these client programs, and may become a basis for dynamic or static program analyses. For a certain class of consistency models specifications, we prove a full abstraction result that connects the two styles of specifications.},
Thomas Wood's avatar
Thomas Wood committed
112
  doi       = {10.4230/LIPIcs.CONCUR.2017.26},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
113 114 115 116 117 118 119 120 121 122 123
  file      = {:Cerone2017Algebraic.pdf:PDF},
  project   = { concurrency },
}

@InProceedings{DOsualdo2017Deciding,
  author    = {Emanuele D'Osualdo and Luke Ong and Alwen Tiu},
  title     = {Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes},
  booktitle = {Proceedings of 30\textsuperscript{th} {IEEE} Computer Security Foundations Symposium, {(CSF 2017)}},
  year      = {2017},
  month     = aug,
  abstract  = {We introduce a new class of security protocols with an unbounded number of sessions and unlimited fresh data for which the problem of secrecy is decidable. The only constraint we place on the class is a notion of depth-boundedness. Precisely we prove that, restricted to messages of up to a given size, secrecy is decidable for all depth-bounded processes. This decidable fragment of security protocols captures many realworld symmetric key protocols, including Needham-SchroederSymmetric Key, Otway-Rees, and Yahalom.},
Thomas Wood's avatar
Thomas Wood committed
124
  doi       = {10.1109/CSF.2017.32},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
125 126 127 128
  file      = {DOsualdo2017Deciding.pdf:DOsualdo2017Deciding.pdf:PDF},
  project   = {concurrency},
}

129
@Proceedings{Felleisen2013Programming,
130
  title     = {Programming Languages and Systems},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
131
  year      = {2013},
132
  booktitle = {Programming Languages and Systems - 22\textsuperscript{nd} European Symposium on Programming, {ESOP} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
133 134 135 136 137 138 139 140
  editor    = {Matthias Felleisen and Philippa Gardner},
  volume    = {7792},
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn      = {978-3-642-37035-9},
  doi       = {10.1007/978-3-642-37036-6},
}

141 142
@Article{Cardelli2012Processes,
  author  = {Luca Cardelli and Philippa Gardner},
143
  title   = {Processes in Space},
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
  journal = {Theor. Comput. Sci.},
  year    = {2012},
  volume  = {431},
  pages   = {40--55},
  doi     = {10.1016/j.tcs.2011.12.051},
}

@Article{Benedikt2010Report,
  author  = {Michael Benedikt and Daniela Florescu and Philippa Gardner and Giovanna Guerrini and Marco Mesiti and Emmanuel Waller},
  title   = {Report on the {EDBT/ICDT} 2010 workshop on updates in {XML}},
  journal = {{SIGMOD} Record},
  year    = {2010},
  volume  = {39},
  number  = {1},
  pages   = {54--57},
  doi     = {10.1145/1860702.1860713},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
160 161
}

162
@InProceedings{Cardelli2010Processes,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
163 164
  author    = {Luca Cardelli and Philippa Gardner},
  title     = {Processes in Space},
165
  booktitle = {Programs, Proofs, Processes, 6\textsuperscript{th} Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 - July 4, 2010. Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
166 167 168 169 170 171 172 173 174
  year      = {2010},
  editor    = {Fernando Ferreira and Benedikt L{\"{o}}we and Elvira Mayordomo and Lu{\'{\i}}s Mendes Gomes},
  volume    = {6158},
  series    = {Lecture Notes in Computer Science},
  pages     = {78--87},
  publisher = {Springer},
  doi       = {10.1007/978-3-642-13962-8_9},
}

175 176 177 178 179 180 181 182 183 184 185 186
@Article{Cardelli2009Process,
  author  = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
  title   = {A Process Model of Actin Polymerisation},
  journal = {Electr. Notes Theor. Comput. Sci.},
  year    = {2009},
  volume  = {229},
  number  = {1},
  pages   = {127--144},
  doi     = {10.1016/j.entcs.2009.02.009},
}

@Proceedings{Gardner2009Database,
187
  title     = {Database Programming Languages},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
188
  year      = {2009},
189
  booktitle = {Database Programming Languages - {DBPL} 2009, 12\textsuperscript{th} International Symposium, Lyon, France, August 24, 2009. Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
190 191 192 193 194 195 196 197
  editor    = {Philippa Gardner and Floris Geerts},
  volume    = {5708},
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn      = {978-3-642-03792-4},
  doi       = {10.1007/978-3-642-03793-1},
}

198 199 200 201 202 203 204 205 206 207 208 209
@Article{Cardelli2008Process,
  author  = {Luca Cardelli and Philippa Gardner and Ozan Kahramanogullari},
  title   = {A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis},
  journal = {Electr. Notes Theor. Comput. Sci.},
  year    = {2008},
  volume  = {194},
  number  = {3},
  pages   = {87--102},
  doi     = {10.1016/j.entcs.2007.12.007},
}

@Article{Gardner2007Linear,
210
  author   = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
211
  title    = {Linear Forwarders},
212 213 214 215 216 217 218 219 220 221 222
  journal  = {Inf. Comput.},
  year     = {2007},
  volume   = {205},
  number   = {10},
  pages    = {1526--1550},
  month    = feb,
  abstract = {A \emph{linear forwarder} is a process that receives one message on a channel and sends it on a different channel. We use linear forwarders to provide a distributed implementation of Milner’s asynchronous pi calculus. Such a distributed implementation is known to be difficult due to \emph{input capability}, where a received name is used as the subject of a subsequent input. This allows the dynamic creation of large input processes in the wrong place, thus requiring comparatively large code migrations in order to avoid consensus problems. Linear forwarders constitute a small atom of \emph{input capability} that is easy to move.

We show that the full input capability can be simply encoded using linear forwarders. We also design a distributed machine, demonstrating the ease with which we can implement the pi calculus using linear forwarders. We also show that linear forwarders allow for a simple encoding of distributed choice and have “clean” behaviour in the presence of failures.},
  doi      = {10.1016/j.ic.2007.01.006},
  file     = {:Gardner2007Linear.pdf:PDF},
223 224 225 226 227 228 229 230 231
}

@Article{Zarfaty2006Local,
  author  = {Uri Zarfaty and Philippa Gardner},
  title   = {Local Reasoning About Tree Update},
  journal = {Electr. Notes Theor. Comput. Sci.},
  year    = {2006},
  volume  = {158},
  pages   = {399--424},
232
  month   = may,
233
  doi     = {10.1016/j.entcs.2006.04.020},
234
  file    = {Zarfaty2006Local.pdf:Zarfaty2006Local.pdf:PDF},
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
}

@Article{Gardner2006Editorial,
  author  = {Philippa Gardner and Nobuko Yoshida},
  title   = {Editorial},
  journal = {Theor. Comput. Sci.},
  year    = {2006},
  volume  = {358},
  number  = {2-3},
  pages   = {149},
  doi     = {10.1016/j.tcs.2006.01.013},
}

@Article{Wischik2005Explicit,
  author  = {Lucian Wischik and Philippa Gardner},
250
  title   = {Explicit Fusions},
251 252 253 254 255
  journal = {Theor. Comput. Sci.},
  year    = {2005},
  volume  = {340},
  number  = {3},
  pages   = {606--630},
256
  month   = aug,
257
  doi     = {10.1016/j.tcs.2005.03.017},
258
  file    = {Wischik2005Explicit.pdf:Wischik2005Explicit.pdf:PDF},
259 260
}

261 262 263 264 265 266 267 268 269 270 271 272
@inProceedings{Koenig2005Graph,
  author =	{Barbara K{\"o}nig and Ugo Montanari and Philippa Gardner},
  title =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  booktitle =	{04241 Abstracts Collection -- Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  year =	{2005},
  editor =	{Barbara K{\"o}nig and Ugo Montanari and Philippa Gardner},
  number =	{04241},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher ={Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2005/27},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
273 274
}

275
@InProceedings{Wischik2004Strong,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
276 277
  author    = {Lucian Wischik and Philippa Gardner},
  title     = {Strong Bisimulation for the Explicit Fusion Calculus},
278
  booktitle = {Foundations of Software Science and Computation Structures, 7\textsuperscript{th} International Conference, {FOSSACS} 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
279 280 281 282 283
  year      = {2004},
  editor    = {Igor Walukiewicz},
  volume    = {2987},
  series    = {Lecture Notes in Computer Science},
  pages     = {484--498},
284
  month     = mar,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
285 286
  publisher = {Springer},
  doi       = {10.1007/978-3-540-24727-2_34},
287
  file      = {Wischik2004Strong.pdf:Wischik2004Strong.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
288 289
}

290
@InProceedings{Gardner2003Linear,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
291 292
  author    = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
  title     = {Linear Forwarders},
293
  booktitle = {{CONCUR} 2003 - Concurrency Theory, 14\textsuperscript{th} International Conference, Marseille, France, September 3-5, 2003, Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
294 295 296 297 298
  year      = {2003},
  editor    = {Roberto M. Amadio and Denis Lugiez},
  volume    = {2761},
  series    = {Lecture Notes in Computer Science},
  pages     = {408--422},
299
  month     = sep,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
300 301
  publisher = {Springer},
  doi       = {10.1007/978-3-540-45187-7_27},
302
  file      = {:Gardner2003Linear.extended.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
303 304
}

305
@InProceedings{Gardner2002Fusion,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
306 307
  author    = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
  title     = {The Fusion Machine},
308
  booktitle = {{CONCUR} 2002 - Concurrency Theory, 13\textsuperscript{th} International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
309 310 311 312 313
  year      = {2002},
  editor    = {Lubos Brim and Petr Jancar and Mojm{\'{\i}}r Kret{\'{\i}}nsk{\'{y}} and Anton{\'{\i}}n Kucera},
  volume    = {2421},
  series    = {Lecture Notes in Computer Science},
  pages     = {418--433},
314
  month     = aug,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
315 316
  publisher = {Springer},
  doi       = {10.1007/3-540-45694-5_28},
317
  file      = {Gardner2002Fusion.pdf:Gardner2002Fusion.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
318 319
}

320
@InProceedings{Gardner2000Process,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
321 322
  author    = {Philippa Gardner},
  title     = {From Process Calculi to Process Frameworks},
323
  booktitle = {{CONCUR} 2000 - Concurrency Theory, 11\textsuperscript{th} International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
324 325 326 327 328 329 330
  year      = {2000},
  editor    = {Catuscia Palamidessi},
  volume    = {1877},
  series    = {Lecture Notes in Computer Science},
  pages     = {69--88},
  publisher = {Springer},
  doi       = {10.1007/3-540-44618-4_7},
331
  file      = {Gardner2000Process.pdf:Gardner2000Process.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
332 333
}

334
@InProceedings{Gardner2000Explicit,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
335 336
  author    = {Philippa Gardner and Lucian Wischik},
  title     = {Explicit Fusions},
337
  booktitle = {Mathematical Foundations of Computer Science 2000, 25\textsuperscript{th} International Symposium, {MFCS} 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
338 339 340 341 342
  year      = {2000},
  editor    = {Mogens Nielsen and Branislav Rovan},
  volume    = {1893},
  series    = {Lecture Notes in Computer Science},
  pages     = {373--382},
343
  month     = aug,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
344 345
  publisher = {Springer},
  doi       = {10.1007/3-540-44612-5_33},
346
  file      = {Gardner2000Explicit.pdf:Gardner2000Explicit.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
347 348
}

349 350 351 352 353 354 355 356 357
@Article{Gardner1999Closed,
  author  = {Philippa Gardner},
  title   = {Closed Action Calculi},
  journal = {Theor. Comput. Sci.},
  year    = {1999},
  volume  = {228},
  number  = {1-2},
  pages   = {77--103},
  doi     = {10.1016/S0304-3975(98)00355-7},
358
  file    = {Gardner1999Closed.pdf:Gardner1999Closed.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
359 360
}

361 362 363 364 365 366 367 368
@Article{Gardner1997Type,
  author  = {Philippa Gardner},
  title   = {A Type-theoretic Description of Action Calculi},
  journal = {Electr. Notes Theor. Comput. Sci.},
  year    = {1997},
  volume  = {10},
  pages   = {52},
  doi     = {10.1016/S1571-0661(05)82513-7},
369
  file    = {Gardner1997Type.pdf:Gardner1997Type.pdf:PDF},
370 371 372
}

@InProceedings{Barber1997Action,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
373 374
  author    = {Andrew G. Barber and Philippa Gardner and Masahito Hasegawa and Gordon D. Plotkin},
  title     = {From Action Calculi to Linear Logic},
375
  booktitle = {Computer Science Logic, 11\textsuperscript{th} International Workshop, {CSL} '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
376 377 378 379 380 381 382
  year      = {1997},
  editor    = {Mogens Nielsen and Wolfgang Thomas},
  volume    = {1414},
  series    = {Lecture Notes in Computer Science},
  pages     = {78--97},
  publisher = {Springer},
  doi       = {10.1007/BFb0028008},
383
  file      = {Barber1997Action.pdf:Barber1997Action.pdf:PDF;Barber1997Action.ps:Barber1997Action.ps:PostScript},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
384 385
}

386
@InProceedings{Gardner1997Types,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
387 388 389 390 391 392 393 394 395 396
  author    = {Philippa Gardner and Masahito Hasegawa},
  title     = {Types and Models for Higher-Order Action Calculi},
  booktitle = {Theoretical Aspects of Computer Software, Third International Symposium, {TACS} '97, Sendai, Japan, September 23-26, 1997, Proceedings},
  year      = {1997},
  editor    = {Mart{\'{\i}}n Abadi and Takayasu Ito},
  volume    = {1281},
  series    = {Lecture Notes in Computer Science},
  pages     = {583--603},
  publisher = {Springer},
  doi       = {10.1007/BFb0014569},
397
  file      = {:Gardner1997Types.extended.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
398 399
}

400
@Article{Gardner1995Name,
401
  author  = {Philippa Gardner},
402
  title   = {A Name-free Account of Action Calculi},
403 404 405 406 407
  journal = {Electr. Notes Theor. Comput. Sci.},
  year    = {1995},
  volume  = {1},
  pages   = {214--231},
  doi     = {10.1016/S1571-0661(04)80012-4},
408
  file    = {Gardner1995Name.pdf:Gardner1995Name.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
409 410
}

411 412 413 414 415 416 417 418 419
@Article{Gardner1995Equivalences,
  author  = {Philippa Gardner},
  title   = {Equivalences between Logics and Their Representing Type Theories},
  journal = {Mathematical Structures in Computer Science},
  year    = {1995},
  volume  = {5},
  number  = {3},
  pages   = {323--349},
  doi     = {10.1017/S0960129500000785},
420
  file    = {Gardner1995Equivalences.pdf:Gardner1995Equivalences.pdf:PDF},
421 422 423
}

@InProceedings{Gardner1994Discovering,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
424 425 426 427 428 429 430 431 432 433
  author    = {Philippa Gardner},
  title     = {Discovering Needed Reductions Using Type Theory},
  booktitle = {Theoretical Aspects of Computer Software, International Conference {TACS} '94, Sendai, Japan, April 19-22, 1994, Proceedings},
  year      = {1994},
  editor    = {Masami Hagiya and John C. Mitchell},
  volume    = {789},
  series    = {Lecture Notes in Computer Science},
  pages     = {555--574},
  publisher = {Springer},
  doi       = {10.1007/3-540-57887-0_115},
434
  file      = {Gardner1994Discovering.pdf:Gardner1994Discovering.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
435 436
}

437 438
@PhdThesis{Gardner1992Representing,
  author = {Philippa Gardner},
439
  title  = {Representing Logics in Type Theory},
440 441
  school = {University of Edinburgh, {UK}},
  year   = {1992},
442
  phdthesis = {Y},
443
  month  = jan,
444
  file   = {Gardner1992Representing.pdf:Gardner1992Representing.pdf:PDF},
445
  url    = {http://hdl.handle.net/1842/14888},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
446 447
}

Thomas Wood's avatar
Thomas Wood committed
448
@Article{Calcagno2010Adjunct,
449 450 451 452 453 454 455 456
  author   = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
  title    = {{Adjunct elimination in Context Logic for Trees}},
  journal  = {Information and Computation},
  year     = {2010},
  volume   = {208},
  number   = {5},
  pages    = {474--499},
  abstract = {We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
457
  doi      = {10.1016/j.ic.2009.02.013},
458 459
  file     = {Calcagno2010Adjunct.pdf:Calcagno2010Adjunct.pdf:PDF},
  project  = { TBD },
Thomas Wood's avatar
Thomas Wood committed
460 461 462
}

@InProceedings{Calcagno2007Adjunct,
463 464 465 466
  author    = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
  title     = {{Adjunct Elimination in Context Logic for Trees}},
  booktitle = {Proceedings of the 5\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS'07})},
  year      = {2007},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
467 468 469
  editor    = {Zhong Shao},
  volume    = {4807},
  series    = {Lecture Notes in Computer Science},
470
  pages     = {255--270},
471
  month     = nov,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
472
  publisher = {Springer},
473
  abstract  = {We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
474
  doi       = {10.1007/978-3-540-76637-7_17},
475 476 477 478 479 480 481 482 483
  file      = {Calcagno2007Adjunct.pdf:Calcagno2007Adjunct.pdf:PDF},
  project   = { TBD },
}

@InProceedings{Calcagno2005Separation,
  author    = {Cristiano Calcagno and Philippa Gardner and Matthew Hague},
  title     = {{From Separation Logic to First-Order Logic}},
  booktitle = {Proceedings of the 8\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS'05})},
  year      = {2005},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
484 485 486
  editor    = {Vladimiro Sassone},
  volume    = {3441},
  series    = {Lecture Notes in Computer Science},
487
  pages     = {395--409},
488
  month     = apr,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
489
  publisher = {Springer},
490
  abstract  = {Separation logic is a spatial logic for reasoning locally about heap structures. A decidable fragment of its assertion language was presented in [3], based on a bounded model property. We exploit this property to give an encoding of this fragment into a first-order logic containing only the propositional connectives, quantification over the natural numbers and equality. This result is the first translation from Separation Logic into a logic which does not depend on the heap, and provides a direct decision procedure based on well-studied algorithms for first-order logic. Moreover, our translation is compositional in the structure of formulae, whilst previous results involved enumerating either heaps or formulae arising from the bounded model property.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
491
  doi       = {10.1007/978-3-540-31982-5_25},
492 493
  file      = {Calcagno2005From.pdf:Calcagno2005Separation.pdf:PDF},
  project   = { TBD },
Thomas Wood's avatar
Thomas Wood committed
494 495 496
}

@InProceedings{Calcagno2007Context,
497 498 499 500
  author    = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
  title     = {{Context Logic as Modal Logic: Completeness and Parametric Inexpressivity}},
  booktitle = {Proceedings of the 34\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'07})},
  year      = {2007},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
501
  editor    = {Martin Hofmann and Matthias Felleisen},
502
  pages     = {123--134},
503
  month     = jan,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
504
  publisher = {{ACM}},
505
  abstract  = {Separation Logic, Ambient Logic and Context Logic are based on a similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret these structural connectives as modalities in Modal Logic and prove completeness results. The structural connectives are essential for describing properties of the underlying data, such as weakest preconditions for Hoare reasoning for Separation and Context Logic, and security properties for Ambient Logic. In fact, we introduced Context Logic to reason about tree update, precisely because the structural connectives of the Ambient Logic did not have enough expressive power. Despite these connectives being essential, first Lozes then Dawar, Gardner and Ghelli proved elimination results for Separation Logic and Ambient Logic (without quantifiers). In this paper, we solve this apparent contradiction. We study parametric inexpressivity results, which demonstrate that the structural connectives are indeed fundamental for this style of reasoning.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
506
  doi       = {10.1145/1190216.1190236},
507
  file      = {Calcagno2007Context.pdf:Calcagno2007Context.pdf:PDF},
508
  project   = {TBD},
Thomas Wood's avatar
Thomas Wood committed
509 510 511
}

@Article{Calcagno2007Local,
512 513 514 515 516 517
  author   = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
  title    = {{Local Reasoning about Data Update}},
  journal  = {Electronic Notes on Theoretical Computer Science},
  year     = {2007},
  volume   = {172},
  pages    = {133--175},
518
  month    = apr,
519
  abstract = {We present local Hoare reasoning about data update, using Context Logic for analysing structured data. We apply our reasoning to tree update, heap update which is analogous to local Hoare reasoning using Separation Logic, and term rewriting.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
520
  doi      = {10.1016/j.entcs.2007.02.006},
521 522
  file     = {Calcagno2007Local.pdf:Calcagno2007Local.pdf:PDF},
  project  = { TBD },
Thomas Wood's avatar
Thomas Wood committed
523 524 525
}

@InProceedings{Calcagno2005Context,
526 527 528 529
  author    = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
  title     = {{Context Logic and Tree Update}},
  booktitle = {Proceedings of the 32\textsuperscript{nd} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'05})},
  year      = {2005},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
530
  editor    = {Jens Palsberg and Mart{\'{\i}}n Abadi},
531
  pages     = {271--282},
532
  month     = jan,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
533
  publisher = {{ACM}},
534
  abstract  = {Spatial logics have been used to describe properties of tree-like structures (Ambient Logic) and in a Hoare style to reason about dynamic updates of heap-like structures (Separation Logic). We integrate this work by analysing dynamic updates to tree-like structures with pointers (such as XML with identifiers and idrefs). Naive adaptations of the Ambient Logic are not expressive enough to capture such local updates. Instead we must explicitly reason about arbitrary tree contexts in order to capture updates throughout the tree. We introduce Context Logic, study its proof theory and models, and show how it generalizes Separation Logic and its general theory BI. We use it to reason locally about a small imperative programming language for updating trees, using a Hoare logic in the style of O'Hearn, Reynolds and Yang, and show that weakest preconditions are derivable. We demonstrate the robustness of our approach by using Context Logic to capture the locality of term rewrite systems.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
535
  doi       = {10.1145/1040305.1040328},
536 537
  file      = {Calcagno2005Context.pdf:Calcagno2005Context.pdf:PDF},
  project   = { TBD },
Thomas Wood's avatar
Thomas Wood committed
538 539 540
}

@Article{Cardelli2007Manipulating,
541 542 543 544 545 546
  author   = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
  title    = {{Manipulating Trees with Hidden Labels}},
  journal  = {Electronic Notes in Theoretical Computer Science},
  year     = {2007},
  volume   = {172},
  pages    = {177--201},
547
  month    = apr,
548 549 550 551
  abstract = {We define an operational semantics and a type system for manipulating semistructured data that contains hidden information. The data model is simple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.},
  doi      = {10.1016/j.entcs.2007.02.007},
  file     = {Cardelli2007Manipulating.pdf:Cardelli2007Manipulating.pdf:PDF},
  project  = { TBD },
Thomas Wood's avatar
Thomas Wood committed
552 553 554
}

@InProceedings{Cardelli2003Manipulating,
555 556 557 558
  author    = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
  title     = {{Manipulating Trees with Hidden Labels}},
  booktitle = {Proceedings of the 6\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS'03})},
  year      = {2003},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
559 560 561
  editor    = {Andrew D. Gordon},
  volume    = {2620},
  series    = {Lecture Notes in Computer Science},
562
  pages     = {216--232},
563
  month     = apr,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
564
  publisher = {Springer},
565
  abstract  = {We define an operational semantics and a type system for manipulating semistructured data that contains hidden information. The data model is simple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
566
  doi       = {10.1007/3-540-36576-1_14},
567
  file      = {Cardelli2003Manipulating.pdf:Cardelli2003Manipulating.pdf:PDF},
568
  project   = {TBD},
Thomas Wood's avatar
Thomas Wood committed
569 570 571
}

@InProceedings{Cardelli2002Spatial,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
572 573 574 575 576 577 578 579
  author    = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
  title     = {{A Spatial Logic for Querying Graphs}},
  booktitle = {Proceedings of the 29\textsuperscript{th} International Colloquium on Automata, Languages and Programming ({ICALP'02})},
  year      = {2002},
  editor    = {Peter Widmayer and Francisco Triguero Ruiz and Rafael Morales Bueno and Matthew Hennessy and Stephan Eidenbenz and Ricardo Conejo},
  volume    = {2380},
  series    = {Lecture Notes in Computer Science},
  pages     = {597--610},
580
  month     = jul,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
581 582 583
  publisher = {Springer},
  abstract  = {We study a spatial logic for reasoning about labelled directed graphs, and the application of this logic to provide a query language for analysing and manipulating such graphs. We give a graph description using constructs from process algebra. We introduce a spatial logic in order to reason locally about disjoint subgraphs. We extend our logic to provide a query language which preserves the multiset semantics of our graph model. Our approach contrasts with the more traditional set-based semantics found in query languages such as TQL, Strudel and GraphLog.},
  doi       = {10.1007/3-540-45465-9_51},
584
  file      = {Cardelli2002Spatial.pdf:Cardelli2002Spatial.pdf:PDF},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
585
  project   = { TBD },
Thomas Wood's avatar
Thomas Wood committed
586 587 588
}

@Article{Dawar2007Expressiveness,
589 590 591 592 593 594 595
  author   = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
  title    = {{Expressiveness and Complexity of Graph Logic}},
  journal  = {Information and Computation},
  year     = {2007},
  volume   = {205},
  number   = {3},
  pages    = {263--310},
596
  month    = feb,
597
  abstract = {We investigate the complexity and expressive power of a spatial logic for reasoning about graphs. This logic was previously introduced by Cardelli, Gardner and Ghelli, and provides the simplest setting in which to explore such results for spatial logics. We study several forms of the logic: the logic with and without recursion, and with either an exponential or a linear version of the basic composition operator. We study the combined complexity and the expressive power of the four combinations. We prove that, without recursion, the linear and exponential versions of the logic correspond to significant fragments of first-order (FO) and monadic second-order (MSO) Logics; the two versions are actually equivalent to FO and MSO on graphs representing strings. However, when the two versions are enriched with mu-style recursion, their expressive power is sharply increased.Both are able to express PSPACE-complete problems, although their combined complexity and data complexity still belong to PSPACE.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
598
  doi      = {10.1016/j.ic.2006.10.006},
599 600
  file     = {Dawar2007Expressiveness.pdf:Dawar2007Expressiveness.pdf:PDF},
  project  = { TBD },
Thomas Wood's avatar
Thomas Wood committed
601 602 603
}

@InProceedings{Dawar2004Adjunct,
604 605 606 607
  author    = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
  title     = {{Adjunct Elimination Through Games in Static Ambient Logic}},
  booktitle = {Proceedings of the 24\textsuperscript{th} International Conference on Foundations of Software Technology and Theoretical Computer Science ({FSTTCS'04})},
  year      = {2004},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
608 609 610
  editor    = {Kamal Lodaya and Meena Mahajan},
  volume    = {3328},
  series    = {Lecture Notes in Computer Science},
611
  pages     = {211--223},
612
  month     = dec,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
613
  publisher = {Springer},
614
  abstract  = {Spatial logics are used to reason locally about disjoint data structures. They consist of standard first-order logic constructs, spatial (structural) connectives and their corresponding adjuncts. Lozes has shown that the adjuncts add no expressive power to a spatial logic for analysing tree structures, a surprising and important result. He also showed that a related logic does not have this adjunct elimination property. His proofs yield little information on the generality of adjunct elimination. We present a new proof of these results based on model-comparison games, and strengthen Lozes' results. Our proof is directed by the intuition that adjuncts can be eliminated when the corresponding moves are not useful in winning the game. The proof is modular with respect to the operators of the logic, providing a general technique for determining which combinations of operators admit adjunct elimination.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
615
  doi       = {10.1007/978-3-540-30538-5_18},
616
  file      = {Dawar2004Adjunct.pdf:Dawar2004Adjunct.pdf:PDF;:Dawar2004Adjunct.extended.pdf:PDF},
617
  project   = { TBD },
Thomas Wood's avatar
Thomas Wood committed
618 619 620
}

@InProceedings{Dinsdale-Young2013Views,
621 622 623 624
  author    = {Thomas Dinsdale{-}Young and Lars Birkedal and Philippa Gardner and Matthew J. Parkinson and Hongseok Yang},
  title     = {{Views: Compositional Reasoning for Concurrent Programs}},
  booktitle = {Proceedings of the 40\textsuperscript{th} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'13})},
  year      = {2013},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
625
  editor    = {Roberto Giacobazzi and Radhia Cousot},
626
  pages     = {287--300},
627
  month     = jan,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
628
  publisher = {{ACM}},
629 630
  abstract  = {Compositional abstractions underly many reasoning principles for concurrent programs: the concurrent environment is abstracted in order to reason about a thread in isolation; and these abstractions are composed to reason about a program consisting of many threads. For instance, separation logic uses formulae that describe part of the state, abstracting the rest; when two threads use disjoint state, their specifications can be composed with the separating conjunction. Type systems abstract the state to the types of variables; threads may be composed when they agree on the types of shared variables.
In this paper, we present the 'Concurrent Views Framework', a metatheory of concurrent reasoning principles. The theory is parameterised by an abstraction of state with a notion of composition, which we call views. The metatheory is remarkably simple, but highly applicable: the rely-guarantee method, concurrent separation logic, concurrent abstract predicates, type systems for recursive references and for unique pointers, and even an adaptation of the Owicki-Gries method can all be seen as instances of the Concurrent Views Framework. Moreover, our metatheory proves each of these systems is sound without requiring induction on the operational semantics.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
631
  doi       = {10.1145/2429069.2429104},
632
  file      = {Dinsdale-Young2013Views.pdf:Dinsdale-Young2013Views.pdf:PDF},
633
  project   = {concurrency},
Thomas Wood's avatar
Thomas Wood committed
634 635 636
}

@InProceedings{Dinsdale-Young2010Concurrent,
637 638 639 640
  author    = {Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Matthew J. Parkinson and Viktor Vafeiadis},
  title     = {{Concurrent Abstract Predicates}},
  booktitle = {Proceedings of the 24\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP'10})},
  year      = {2010},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
641 642 643
  editor    = {Theo D'Hondt},
  volume    = {6183},
  series    = {Lecture Notes in Computer Science},
644
  pages     = {504--528},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
645
  publisher = {Springer},
646
  abstract  = {Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a program logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module's implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
647
  doi       = {10.1007/978-3-642-14107-2_24},
648 649
  file      = {Dinsdale-Young2010Concurrent.pdf:Dinsdale-Young2010Concurrent.pdf:PDF},
  project   = { concurrency },
Thomas Wood's avatar
Thomas Wood committed
650 651 652
}

@InProceedings{Dinsdale-Young2011Abstract,
653 654 655 656
  author    = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
  title     = {{Abstract Local Reasoning for Program Modules}},
  booktitle = {Proceedings of the 4\textsuperscript{th} International Conference on Algebra and Coalgebra in Computer Science ({CALCO'11})},
  year      = {2011},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
657 658 659
  editor    = {Andrea Corradini and Bartek Klin and Corina C{\^{\i}}rstea},
  volume    = {6859},
  series    = {Lecture Notes in Computer Science},
660
  pages     = {36--39},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
661
  publisher = {Springer},
662 663
  abstract  = {Hoare logic ([7]) is an important tool for formally proving correctness properties of programs. It takes advantage of modularity by treating program fragments in terms of provable specifications. However, heap programs tend to break this type of modular reasoning by permitting pointer aliasing. For instance, the specification that a program reverses one list does not imply that it leaves a second list alone. To achieve this disjointness property, it is necessary to establish disjointness conditions
throughout the proof.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
664
  doi       = {10.1007/978-3-642-22944-2_3},
665 666
  file      = {Dinsdale-Young2011Abstract.pdf:Dinsdale-Young2011Abstract.pdf:PDF},
  project   = { TBD },
Thomas Wood's avatar
Thomas Wood committed
667 668 669
}

@InProceedings{Dinsdale-Young2010Abstraction,
670 671 672 673
  author    = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
  title     = {{Abstraction and Refinement for Local Reasoning}},
  booktitle = {Proceedings of the 3\textsuperscript{rd} International Conference on Verified Software: Theories, Tools, Experiments ({VSTTE'10})},
  year      = {2010},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
674 675 676
  editor    = {Gary T. Leavens and Peter W. O'Hearn and Sriram K. Rajamani},
  volume    = {6217},
  series    = {Lecture Notes in Computer Science},
677
  pages     = {199--215},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
678
  publisher = {Springer},
679
  abstract  = {Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state. We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations. We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level`fiction' of locality.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
680
  doi       = {10.1007/978-3-642-15057-9_14},
681
  file      = {Dinsdale-Young2010Abstraction.pdf:Dinsdale-Young2010Abstraction.pdf:PDF;:Dinsdale-Young2010Abstraction.techreport.pdf:PDF},
682
  project   = { TBD },
Thomas Wood's avatar
Thomas Wood committed
683 684 685
}

@InProceedings{Gardner2010Reasoning,
686 687 688 689
  author    = {Philippa Gardner},
  title     = {{Reasoning About Client-side Web Programs: Invited Talk}},
  booktitle = {Proceedings of the 2010 {EDBT/ICDT} Workshops},
  year      = {2010},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
690 691 692
  editor    = {Florian Daniel and Lois M. L. Delcambre and Farshad Fotouhi and Irene Garrig{\'{o}}s and Giovanna Guerrini and Jose{-}Norberto Maz{\'{o}}n and Marco Mesiti and Sascha M{\"{u}}ller and Juan Trujillo and Traian Marius Truta and Bernhard Volz and Emmanuel Waller and Li Xiong and Esteban Zim{\'{a}}nyi},
  series    = {{ACM} International Conference Proceeding Series},
  publisher = {{ACM}},
693 694 695 696
  abstract  = {In PODS 2008, I presented a paper on a formal, compositional specification of the Document Object Model (DOM), a W3C XML Update library. This work concentrated on Featherweight DOM, a small fragment of DOM which focuses on the XML tree structure and simple text nodes. Since the formal reasoning is compositional, we are able to work with a minimal set of commands and obtain complete reasoning for straight-line code. We are also able to verify, for example, invariant properties of simple DOM programs. This work is based on a recent breakthrough in program verification, based on analysing a program's use of resource. The idea is that the reasoning should follow the programmers' intuitions about which part of the computer memory the program touches. This style of reasoning was introduced by O'Hearn (Queen Mary) and Reynolds (CMU) in their work on Separation Logic for reasoning modularly about large C-programs (e.g. Microsoft device driver code, Linux). I substantially extended the range of local resource reasoning, introducing Context Logic to reason about programs that directly manipulate complex data structures such as XML. In this survey talk, I will give an overview of our theoretical and practical work on reasoning about DOM, highlighting recent developments which include: 1. the extension of this work to DOM Core Level 1. A substantial piece of work, not because of the reasoning, but because full DOM is large, underspecified and difficult to interpret, with no consensus between browsers; 2. reasoning about the combination of JavaScript and DOM to provide, for example, secure mashups for a more flexible, secure integration of outsourced payment services; 3. on-going work on a verification tool for automatically reasoning about DOM programs and the identification of key examples of web applications on which to test our DOM reasoning: e.g., with current technology, we can prove by hand that mashup programs are fault free; with our tool, such proofs will be automatic. An ultimate challenge is to develop the necessary reasoning technology to provide a safe and secure web environment on which to build the next generation of web applications, thus demonstrating the scientific feasibility of a reliable Web.},
  doi       = {10.1145/1754239.1754261},
  file      = {Gardner2010Reasoning.pdf:Gardner2010Reasoning.pdf:PDF},
  project   = { web },
Thomas Wood's avatar
Thomas Wood committed
697 698 699
}

@Article{Gardner2005Modelling,
700 701 702 703 704 705 706
  author   = {Philippa Gardner and Sergio Maffeis},
  title    = {{Modelling Dynamic Web Data}},
  journal  = {Theoretical Computer Science},
  year     = {2005},
  volume   = {342},
  number   = {1},
  pages    = {104--131},
707
  month    = sep,
708
  abstract = {We introduce Xd$\pi$, a peer-to-peer model for reasoning about the dynamic behaviour of web data. It is based on an idealised model of semi-structured data, and an extension of the $\pi$-calculus with process mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found in, for example, dynamic web page programming, applet interaction, and service orchestration. We study behavioural equivalences for Xd$\pi$, motivated by examples.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
709
  doi      = {10.1016/j.tcs.2005.06.006},
710 711
  file     = {Gardner2005Modelling.pdf:Gardner2005Modelling.pdf:PDF},
  project  = { web },
Thomas Wood's avatar
Thomas Wood committed
712 713 714
}

@InProceedings{Gardner2003Modelling,
715 716 717 718
  author    = {Philippa Gardner and Sergio Maffeis},
  title     = {{Modelling Dynamic Web Data}},
  booktitle = {Proceedings of 9\textsuperscript{th} International Workshop on Database Programming Languages ({DBPL'03})},
  year      = {2003},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
719 720 721
  editor    = {Georg Lausen and Dan Suciu},
  volume    = {2921},
  series    = {Lecture Notes in Computer Science},
722
  pages     = {130--146},
723
  month     = sep,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
724
  publisher = {Springer},
725
  abstract  = {We introduce Xd$\pi$, a peer-to-peer model for reasoning about the dynamic behaviour of web
pmaksimo's avatar
pmaksimo committed
726
 data. It is based on an idealised model of semi-structured data, and an extension of the pi-calculus with process
Thomas Wood's avatar
Thomas Wood committed
727
 mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found
pmaksimo's avatar
pmaksimo committed
728
 in, for example, dynamic web page programming, applet interaction, and service orchestration. We study
729
 behavioural equivalences for Xd$\pi$, motivated by examples.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
730
  doi       = {10.1007/978-3-540-24607-7_9},
731 732
  file      = {Gardner2003Modelling.pdf:Gardner2003Modelling.pdf:PDF},
  project   = { web },
Thomas Wood's avatar
Thomas Wood committed
733 734 735
}

@InProceedings{Gardner2012Towards,
736 737 738 739
  author    = {Philippa Gardner and Sergio Maffeis and Gareth Smith},
  title     = {{Towards a Program Logic for JavaScript}},
  booktitle = {Proceedings of the 39\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL'12})},
  year      = {2012},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
740
  editor    = {John Field and Michael Hicks},
741
  pages     = {31--44},
742
  month     = jan,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
743
  publisher = {{ACM}},
744
  abstract  = {JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts.
745

746
We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with. We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
747
  doi       = {10.1145/2103656.2103663},
748
  file      = {Gardner2012Towards.pdf:Gardner2012Towards.pdf:PDF},
749
  project   = {web},
Thomas Wood's avatar
Thomas Wood committed
750 751 752
}

@InProceedings{Gardner2014Local,
753 754 755 756
  author    = {Philippa Gardner and Gian Ntzik and Adam Wright},
  title     = {{Local Reasoning for the {POSIX} File System}},
  booktitle = {Proceedings of the 23\textsuperscript{rd} European Symposium on Programming ({ESOP'14})},
  year      = {2014},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
757 758 759
  editor    = {Zhong Shao},
  volume    = {8410},
  series    = {Lecture Notes in Computer Science},
760
  pages     = {169--188},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
761
  publisher = {Springer},
762
  abstract  = {We provide a program logic for specifying a core subset of the sequential POSIX file system, and for reasoning abstractly about client programs working with the file system.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
763
  doi       = {10.1007/978-3-642-54833-8_10},
764 765
  file      = {Gardner2014Local.pdf:Gardner2014Local.pdf:PDF},
  project   = { concurrency },
Thomas Wood's avatar
Thomas Wood committed
766 767 768
}

@Article{Gardner2014Abstract,
769 770 771 772 773 774 775
  author   = {Philippa Gardner and Azalea Raad and Mark J. Wheelhouse and Adam Wright},
  title    = {{Abstract Local Reasoning for Concurrent Libraries: Mind the Gap}},
  journal  = {Proceedings of the 30\textsuperscript{th} Conference on the Mathematical Foundations of Programming Semantics ({MFPS'14})},
  year     = {2014},
  volume   = {308},
  pages    = {147--166},
  abstract = {We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
776
  doi      = {10.1016/j.entcs.2014.10.009},
777 778
  file     = {Gardner2014Abstract.pdf:Gardner2014Abstract.pdf:PDF},
  project  = { concurrency },
Thomas Wood's avatar
Thomas Wood committed
779 780 781
}

@InProceedings{Gardner2008DOM,
782 783 784 785 786 787 788
  author    = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
  title     = {{DOM: Towards a Formal Specification}},
  booktitle = {Proceedings of the {ACM} {SIGPLAN} Workshop on Programming Language Technologies for XML ({PLAN-X'08})},
  year      = {2008},
  abstract  = {The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O'Hearn, Reynolds and Yang's local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g. invariant properties of simple Javascript programs.},
  file      = {Gardner2008DOM.pdf:Gardner2008DOM.pdf:PDF},
  project   = { web },
Thomas Wood's avatar
Thomas Wood committed
789 790 791
}

@InProceedings{Gardner2008Local,
792 793 794 795
  author    = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
  title     = {{Local Hoare Reasoning about {DOM}}},
  booktitle = {Proceedings of the 27\textsuperscript{th} {ACM} {SIGMOD-SIGACT-SIGART} Symposium on Principles of Database Systems ({PODS'08})},
  year      = {2008},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
796
  editor    = {Maurizio Lenzerini and Domenico Lembo},
797
  pages     = {261--270},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
798
  publisher = {{ACM}},
799
  abstract  = {The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O'Hearn, Reynolds and Yang's local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about simple tree update to this real-world DOM application. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify, for example, invariant properties of simple Javascript programs.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
800
  doi       = {10.1145/1376916.1376953},
801 802
  file      = {Gardner2008Local.pdf:Gardner2008Local.pdf:PDF},
  project   = { web },
Thomas Wood's avatar
Thomas Wood committed
803 804 805
}

@InProceedings{Gardner2009Small,
806 807 808 809
  author    = {Philippa Gardner and Mark J. Wheelhouse},
  title     = {{Small Specifications for Tree Update}},
  booktitle = {Proceedings of the 6\textsuperscript{th} International Workshop on Web Services and Formal Methods ({WS-FM'09})},
  year      = {2009},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
810 811 812
  editor    = {Cosimo Laneve and Jianwen Su},
  volume    = {6194},
  series    = {Lecture Notes in Computer Science},
813
  pages     = {178--195},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
814
  publisher = {Springer},
815
  abstract  = {O'Hearn, Reynolds and Yang introduced Separation Logic to provide modular reasoning about simple, mutable data structures in memory. They were able to construct small specifications of programs, by reasoning about the local parts of memory accessed by programs. Gardner, Calcagno and Zarfaty generalised this work, introducing Context Logic to reason about more complex data structures. In particular, they developed a formal,compositional specification of the Document Object Model,a W3C XML update library. Whilst keeping to the spirit of local reasoning, they were not able to retain small specifications. We introduce Segment Logic, which provides a more fine-grained analysis of the tree structure and yields small specifications. As well as being aesthetically pleasing, small specifications are important for reasoning about concurrent tree update.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
816
  doi       = {10.1007/978-3-642-14458-5_11},
817 818
  file      = {Gardner2009Small.pdf:Gardner2009Small.pdf:PDF},
  project   = { TBD },
Thomas Wood's avatar
Thomas Wood committed
819 820 821
}

@InProceedings{Maffeis2004Behavioural,
822 823 824 825
  author    = {Sergio Maffeis and Philippa Gardner},
  title     = {{Behavioural Equivalences for Dynamic Web Data}},
  booktitle = {Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {(TCS'04)}},
  year      = {2004},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
826 827 828
  editor    = {Jean{-}Jacques L{\'{e}}vy and Ernst W. Mayr and John C. Mitchell},
  volume    = {155},
  series    = {{IFIP}},
829
  pages     = {535--548},
830
  month     = aug,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
831
  publisher = {Kluwer/Springer},
832
  abstract  = {We study behavioural equivalences for dynamic web data in Xd$\pi$, a model for reasoning about behaviour found in (for example) dynamic web page programming, applet interaction, and web-service orchestration. Xd$\pi$ is based on an idealised model of semistructured data, and an extension of the 7r-calculus with locations and operations for interacting with data. The equivalences are nonstandard due to the integration of data and processes, and the presence of locations.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
833
  doi       = {10.1007/1-4020-8141-3_41},
834 835
  file      = {Maffeis2004Behavioural.pdf:Maffeis2004Behavioural.pdf:PDF},
  project   = { web },
Thomas Wood's avatar
Thomas Wood committed
836 837 838
}

@InProceedings{Ntzik2015Reasoning,
839 840 841 842
  author    = {Gian Ntzik and Philippa Gardner},
  title     = {{Reasoning about the POSIX File System: Local Update and Global Pathnames}},
  booktitle = {Proceedings of the 30\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA'15})},
  year      = {2015},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
843
  editor    = {Jonathan Aldrich and Patrick Eugster},
844 845
  pages     = {201--220},
  month     = oct,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
846
  publisher = {{ACM}},
847
  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 being 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.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
848
  doi       = {10.1145/2814270.2814306},
849 850
  file      = {Ntzik2015Reasoning.pdf:Ntzik2015Reasoning.pdf:PDF},
  project   = { concurrency },
Thomas Wood's avatar
Thomas Wood committed
851 852 853
}

@InProceedings{Ntzik2015Fault,
854 855 856 857
  author    = {Gian Ntzik and Pedro {da Rocha Pinto} and Philippa Gardner},
  title     = {{Fault-tolerant Resource Reasoning}},
  booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS'15})},
  year      = {2015},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
858 859 860
  editor    = {Xinyu Feng and Sungwoo Park},
  volume    = {9458},
  series    = {Lecture Notes in Computer Science},
861 862
  pages     = {169--188},
  month     = dec,
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
863
  publisher = {Springer},
864 865
  abstract  = {Separation logic has been successful at verifying that programs 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.},
  doi       = {10.1007/978-3-319-26529-2_10},
866
  file      = {Ntzik2015Fault.pdf:Ntzik2015Fault.pdf:PDF},
867
  project   = { concurrency },
Thomas Wood's avatar
Thomas Wood committed
868 869 870
}

@InProceedings{Raad2015CoLoSL,
871 872 873 874
  author    = {Azalea Raad and Jules Villard and Philippa Gardner},
  title     = {{CoLoSL: Concurrent Local Subjective Logic}},
  booktitle = {Proceedings of the 24\textsuperscript{th} European Symposium on Programming ({ESOP'15})},
  year      = {2015},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
875 876 877
  editor    = {Jan Vitek},
  volume    = {9032},
  series    = {Lecture Notes in Computer Science},
878
  pages     = {710--735},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
879
  publisher = {Springer},
880
  abstract  = {A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency typically require reasoning about either the entire shared state or disjoint parts of the shared state, impeding compositionality. This paper introduces the program logic CoLoSL, where each thread is verified with respect to its subjective view of the global shared state. This subjective view describes only that part of the state accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread. This flexibility gives rise to small specifications and, hence, more compositional reasoning for concurrent programs. We demonstrate our reasoning on a range of examples, including a concurrent computation of a spanning tree of a graph.},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
881
  doi       = {10.1007/978-3-662-46669-8_29},
882 883
  file      = {Raad2015CoLoSL.pdf:Raad2015CoLoSL.pdf:PDF},
  project   = { concurrency },
Thomas Wood's avatar
Thomas Wood committed
884 885 886
}

@InProceedings{Raza2009Automatic,
887 888 889 890
  author    = {Mohammad Raza and Cristiano Calcagno and Philippa Gardner},
  title     = {{Automatic Parallelization with Separation Logic}},
  booktitle = {Proceedings of the 18\textsuperscript{th} European Symposium on Programming ({ESOP'09})},
  year      = {2009},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed
891 892 893
  editor    = {Giuseppe Castagna},
  volume    = {5502},
  series    = {Lecture Notes in Computer Science},
894
  pages     = {348--362},
Teresa Carbajo-Garcia's avatar
Teresa Carbajo-Garcia committed