publications.bib 121 KB
Newer Older
 Teresa Carbajo-Garcia committed Apr 04, 2017 1 % Encoding: UTF-8  Thomas Wood committed Feb 03, 2016 2 3  @InProceedings{Bodin2014Trusted,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Mar 09, 2018 11  doi = {10.1145/2535838.2535876},  Teresa Carbajo-Garcia committed Jun 15, 2017 12 13  file = {Bodin2014Trusted.pdf:Bodin2014Trusted.pdf:PDF}, project = { web },  Thomas Wood committed Feb 03, 2016 14 15 }  Teresa Carbajo-Garcia committed Sep 26, 2017 16 17 18 @InProceedings{Raad2016DOM, author = {Azalea Raad and Jos{\'{e}} {Fragoso Santos} and Philippa Gardner}, title = {{DOM:} Specification and Client Reasoning},  Thomas Wood committed Oct 24, 2017 19  booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems (APLAS'16)},  Teresa Carbajo-Garcia committed Sep 26, 2017 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 committed Jul 02, 2018 38  project = { concurrency },  Teresa Carbajo-Garcia committed Sep 26, 2017 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 committed Jul 02, 2018 64  project = { concurrency, tada },  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Teresa Carbajo-Garcia committed Oct 05, 2017 72  month = may,  Teresa Carbajo-Garcia committed Sep 26, 2017 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 committed Jul 02, 2018 77  project = { concurrency, tada },  Teresa Carbajo-Garcia committed Sep 26, 2017 78 79 80 81 82 83 84 } @PhdThesis{Raad2017Abstraction, author = {Azalea Raad}, title = {Abstraction, Refinement and Concurrent Reasoning}, school = {Imperial College London}, year = {2017},  Teresa Carbajo-Garcia committed Oct 05, 2017 85  month = jun,  Teresa Carbajo-Garcia committed Sep 26, 2017 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 committed Oct 04, 2017 100  doi = {10.1007/978-3-319-63046-5_2},  Teresa Carbajo-Garcia committed Sep 26, 2017 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 committed Mar 09, 2018 112  doi = {10.4230/LIPIcs.CONCUR.2017.26},  Teresa Carbajo-Garcia committed Sep 26, 2017 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 committed Mar 09, 2018 124  doi = {10.1109/CSF.2017.32},  Teresa Carbajo-Garcia committed Sep 26, 2017 125 126 127 128  file = {DOsualdo2017Deciding.pdf:DOsualdo2017Deciding.pdf:PDF}, project = {concurrency}, }  Thomas Wood committed Oct 24, 2017 129 @Proceedings{Felleisen2013Programming,  Teresa Carbajo-Garcia committed Jun 14, 2018 130  title = {Programming Languages and Systems},  Teresa Carbajo-Garcia committed Sep 26, 2017 131  year = {2013},  Teresa Carbajo-Garcia committed Jun 14, 2018 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 committed Sep 26, 2017 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}, }  Thomas Wood committed Oct 24, 2017 141 142 @Article{Cardelli2012Processes, author = {Luca Cardelli and Philippa Gardner},  Teresa Carbajo-Garcia committed Jun 14, 2018 143  title = {Processes in Space},  Thomas Wood committed Oct 24, 2017 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 committed Sep 26, 2017 160 161 }  Thomas Wood committed Oct 24, 2017 162 @InProceedings{Cardelli2010Processes,  Teresa Carbajo-Garcia committed Sep 26, 2017 163 164  author = {Luca Cardelli and Philippa Gardner}, title = {Processes in Space},  Thomas Wood committed Oct 24, 2017 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 committed Sep 26, 2017 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}, }  Thomas Wood committed Oct 24, 2017 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,  Teresa Carbajo-Garcia committed Jun 14, 2018 187  title = {Database Programming Languages},  Teresa Carbajo-Garcia committed Sep 26, 2017 188  year = {2009},  Teresa Carbajo-Garcia committed Jun 14, 2018 189  booktitle = {Database Programming Languages - {DBPL} 2009, 12\textsuperscript{th} International Symposium, Lyon, France, August 24, 2009. Proceedings},  Teresa Carbajo-Garcia committed Sep 26, 2017 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}, }  Thomas Wood committed Oct 24, 2017 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,  Thomas Wood committed Nov 03, 2017 210  author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},  Teresa Carbajo-Garcia committed Jun 14, 2018 211  title = {Linear Forwarders},  Thomas Wood committed Nov 03, 2017 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},  Thomas Wood committed Oct 24, 2017 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},  Thomas Wood committed Nov 03, 2017 232  month = may,  Thomas Wood committed Oct 24, 2017 233  doi = {10.1016/j.entcs.2006.04.020},  Thomas Wood committed Oct 24, 2017 234  file = {Zarfaty2006Local.pdf:Zarfaty2006Local.pdf:PDF},  Thomas Wood committed Oct 24, 2017 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},  Teresa Carbajo-Garcia committed Jun 14, 2018 250  title = {Explicit Fusions},  Thomas Wood committed Oct 24, 2017 251 252 253 254 255  journal = {Theor. Comput. Sci.}, year = {2005}, volume = {340}, number = {3}, pages = {606--630},  Thomas Wood committed Nov 01, 2017 256  month = aug,  Thomas Wood committed Oct 24, 2017 257  doi = {10.1016/j.tcs.2005.03.017},  Thomas Wood committed Nov 01, 2017 258  file = {Wischik2005Explicit.pdf:Wischik2005Explicit.pdf:PDF},  Thomas Wood committed Oct 24, 2017 259 260 }  Teresa Carbajo-Garcia committed Jun 14, 2018 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 committed Sep 26, 2017 273 274 }  Thomas Wood committed Oct 24, 2017 275 @InProceedings{Wischik2004Strong,  Teresa Carbajo-Garcia committed Sep 26, 2017 276 277  author = {Lucian Wischik and Philippa Gardner}, title = {Strong Bisimulation for the Explicit Fusion Calculus},  Thomas Wood committed Oct 24, 2017 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 committed Sep 26, 2017 279 280 281 282 283  year = {2004}, editor = {Igor Walukiewicz}, volume = {2987}, series = {Lecture Notes in Computer Science}, pages = {484--498},  Thomas Wood committed Nov 03, 2017 284  month = mar,  Teresa Carbajo-Garcia committed Sep 26, 2017 285 286  publisher = {Springer}, doi = {10.1007/978-3-540-24727-2_34},  Thomas Wood committed Oct 24, 2017 287  file = {Wischik2004Strong.pdf:Wischik2004Strong.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 288 289 }  Thomas Wood committed Oct 24, 2017 290 @InProceedings{Gardner2003Linear,  Teresa Carbajo-Garcia committed Sep 26, 2017 291 292  author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik}, title = {Linear Forwarders},  Thomas Wood committed Oct 24, 2017 293  booktitle = {{CONCUR} 2003 - Concurrency Theory, 14\textsuperscript{th} International Conference, Marseille, France, September 3-5, 2003, Proceedings},  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Thomas Wood committed Nov 01, 2017 299  month = sep,  Teresa Carbajo-Garcia committed Sep 26, 2017 300 301  publisher = {Springer}, doi = {10.1007/978-3-540-45187-7_27},  Thomas Wood committed Nov 01, 2017 302  file = {:Gardner2003Linear.extended.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 303 304 }  Thomas Wood committed Oct 24, 2017 305 @InProceedings{Gardner2002Fusion,  Teresa Carbajo-Garcia committed Sep 26, 2017 306 307  author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik}, title = {The Fusion Machine},  Thomas Wood committed Oct 24, 2017 308  booktitle = {{CONCUR} 2002 - Concurrency Theory, 13\textsuperscript{th} International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings},  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Thomas Wood committed Nov 03, 2017 314  month = aug,  Teresa Carbajo-Garcia committed Sep 26, 2017 315 316  publisher = {Springer}, doi = {10.1007/3-540-45694-5_28},  Thomas Wood committed Oct 24, 2017 317  file = {Gardner2002Fusion.pdf:Gardner2002Fusion.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 318 319 }  Thomas Wood committed Oct 24, 2017 320 @InProceedings{Gardner2000Process,  Teresa Carbajo-Garcia committed Sep 26, 2017 321 322  author = {Philippa Gardner}, title = {From Process Calculi to Process Frameworks},  Thomas Wood committed Oct 24, 2017 323  booktitle = {{CONCUR} 2000 - Concurrency Theory, 11\textsuperscript{th} International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings},  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Thomas Wood committed Oct 24, 2017 331  file = {Gardner2000Process.pdf:Gardner2000Process.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 332 333 }  Thomas Wood committed Oct 24, 2017 334 @InProceedings{Gardner2000Explicit,  Teresa Carbajo-Garcia committed Sep 26, 2017 335 336  author = {Philippa Gardner and Lucian Wischik}, title = {Explicit Fusions},  Thomas Wood committed Oct 24, 2017 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 committed Sep 26, 2017 338 339 340 341 342  year = {2000}, editor = {Mogens Nielsen and Branislav Rovan}, volume = {1893}, series = {Lecture Notes in Computer Science}, pages = {373--382},  Thomas Wood committed Nov 01, 2017 343  month = aug,  Teresa Carbajo-Garcia committed Sep 26, 2017 344 345  publisher = {Springer}, doi = {10.1007/3-540-44612-5_33},  Thomas Wood committed Oct 24, 2017 346  file = {Gardner2000Explicit.pdf:Gardner2000Explicit.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 347 348 }  Thomas Wood committed Oct 24, 2017 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},  Thomas Wood committed Oct 24, 2017 358  file = {Gardner1999Closed.pdf:Gardner1999Closed.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 359 360 }  Thomas Wood committed Oct 24, 2017 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},  Thomas Wood committed Oct 30, 2017 369  file = {Gardner1997Type.pdf:Gardner1997Type.pdf:PDF},  Thomas Wood committed Oct 24, 2017 370 371 372 } @InProceedings{Barber1997Action,  Teresa Carbajo-Garcia committed Sep 26, 2017 373 374  author = {Andrew G. Barber and Philippa Gardner and Masahito Hasegawa and Gordon D. Plotkin}, title = {From Action Calculi to Linear Logic},  Thomas Wood committed Oct 24, 2017 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 committed Sep 26, 2017 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},  Thomas Wood committed Oct 24, 2017 383  file = {Barber1997Action.pdf:Barber1997Action.pdf:PDF;Barber1997Action.ps:Barber1997Action.ps:PostScript},  Teresa Carbajo-Garcia committed Sep 26, 2017 384 385 }  Thomas Wood committed Oct 24, 2017 386 @InProceedings{Gardner1997Types,  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Thomas Wood committed Oct 24, 2017 397  file = {:Gardner1997Types.extended.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 398 399 }  Thomas Wood committed Oct 30, 2017 400 @Article{Gardner1995Name,  Thomas Wood committed Oct 24, 2017 401  author = {Philippa Gardner},  Thomas Wood committed Oct 30, 2017 402  title = {A Name-free Account of Action Calculi},  Thomas Wood committed Oct 24, 2017 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},  Thomas Wood committed Oct 30, 2017 408  file = {Gardner1995Name.pdf:Gardner1995Name.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 409 410 }  Thomas Wood committed Oct 24, 2017 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},  Thomas Wood committed Oct 24, 2017 420  file = {Gardner1995Equivalences.pdf:Gardner1995Equivalences.pdf:PDF},  Thomas Wood committed Oct 24, 2017 421 422 423 } @InProceedings{Gardner1994Discovering,  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Thomas Wood committed Oct 24, 2017 434  file = {Gardner1994Discovering.pdf:Gardner1994Discovering.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 435 436 }  Thomas Wood committed Oct 24, 2017 437 438 @PhdThesis{Gardner1992Representing, author = {Philippa Gardner},  Teresa Carbajo-Garcia committed Jun 14, 2018 439  title = {Representing Logics in Type Theory},  Thomas Wood committed Oct 24, 2017 440 441  school = {University of Edinburgh, {UK}}, year = {1992},  Teresa Carbajo-Garcia committed Jan 31, 2018 442  phdthesis = {Y},  Thomas Wood committed Nov 03, 2017 443  month = jan,  Thomas Wood committed Oct 24, 2017 444  file = {Gardner1992Representing.pdf:Gardner1992Representing.pdf:PDF},  Thomas Wood committed Oct 24, 2017 445  url = {http://hdl.handle.net/1842/14888},  Teresa Carbajo-Garcia committed Sep 26, 2017 446 447 }  Thomas Wood committed Feb 03, 2016 448 @Article{Calcagno2010Adjunct,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 457  doi = {10.1016/j.ic.2009.02.013},  Teresa Carbajo-Garcia committed Jun 15, 2017 458 459  file = {Calcagno2010Adjunct.pdf:Calcagno2010Adjunct.pdf:PDF}, project = { TBD },  Thomas Wood committed Feb 03, 2016 460 461 462 } @InProceedings{Calcagno2007Adjunct,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 467 468 469  editor = {Zhong Shao}, volume = {4807}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 470  pages = {255--270},  Thomas Wood committed Nov 03, 2017 471  month = nov,  Teresa Carbajo-Garcia committed Sep 26, 2017 472  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 474  doi = {10.1007/978-3-540-76637-7_17},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 484 485 486  editor = {Vladimiro Sassone}, volume = {3441}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 487  pages = {395--409},  Thomas Wood committed Nov 03, 2017 488  month = apr,  Teresa Carbajo-Garcia committed Sep 26, 2017 489  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 491  doi = {10.1007/978-3-540-31982-5_25},  Teresa Carbajo-Garcia committed Jun 15, 2017 492 493  file = {Calcagno2005From.pdf:Calcagno2005Separation.pdf:PDF}, project = { TBD },  Thomas Wood committed Feb 03, 2016 494 495 496 } @InProceedings{Calcagno2007Context,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 501  editor = {Martin Hofmann and Matthias Felleisen},  Teresa Carbajo-Garcia committed Jun 15, 2017 502  pages = {123--134},  Thomas Wood committed Nov 03, 2017 503  month = jan,  Teresa Carbajo-Garcia committed Sep 26, 2017 504  publisher = {{ACM}},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 506  doi = {10.1145/1190216.1190236},  Teresa Carbajo-Garcia committed Jun 15, 2017 507  file = {Calcagno2007Context.pdf:Calcagno2007Context.pdf:PDF},  Thomas Wood committed Nov 03, 2017 508  project = {TBD},  Thomas Wood committed Feb 03, 2016 509 510 511 } @Article{Calcagno2007Local,  Teresa Carbajo-Garcia committed Jun 15, 2017 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},  Thomas Wood committed Nov 03, 2017 518  month = apr,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 520  doi = {10.1016/j.entcs.2007.02.006},  Teresa Carbajo-Garcia committed Jun 15, 2017 521 522  file = {Calcagno2007Local.pdf:Calcagno2007Local.pdf:PDF}, project = { TBD },  Thomas Wood committed Feb 03, 2016 523 524 525 } @InProceedings{Calcagno2005Context,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 530  editor = {Jens Palsberg and Mart{\'{\i}}n Abadi},  Teresa Carbajo-Garcia committed Jun 15, 2017 531  pages = {271--282},  Thomas Wood committed Nov 03, 2017 532  month = jan,  Teresa Carbajo-Garcia committed Sep 26, 2017 533  publisher = {{ACM}},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 535  doi = {10.1145/1040305.1040328},  Teresa Carbajo-Garcia committed Jun 15, 2017 536 537  file = {Calcagno2005Context.pdf:Calcagno2005Context.pdf:PDF}, project = { TBD },  Thomas Wood committed Feb 03, 2016 538 539 540 } @Article{Cardelli2007Manipulating,  Teresa Carbajo-Garcia committed Jun 15, 2017 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},  Thomas Wood committed Nov 03, 2017 547  month = apr,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Feb 03, 2016 552 553 554 } @InProceedings{Cardelli2003Manipulating,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 559 560 561  editor = {Andrew D. Gordon}, volume = {2620}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 562  pages = {216--232},  Thomas Wood committed Nov 03, 2017 563  month = apr,  Teresa Carbajo-Garcia committed Sep 26, 2017 564  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 566  doi = {10.1007/3-540-36576-1_14},  Teresa Carbajo-Garcia committed Jun 15, 2017 567  file = {Cardelli2003Manipulating.pdf:Cardelli2003Manipulating.pdf:PDF},  Thomas Wood committed Nov 03, 2017 568  project = {TBD},  Thomas Wood committed Feb 03, 2016 569 570 571 } @InProceedings{Cardelli2002Spatial,  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Thomas Wood committed Nov 03, 2017 580  month = jul,  Teresa Carbajo-Garcia committed Sep 26, 2017 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},  Thomas Wood committed Oct 24, 2017 584  file = {Cardelli2002Spatial.pdf:Cardelli2002Spatial.pdf:PDF},  Teresa Carbajo-Garcia committed Sep 26, 2017 585  project = { TBD },  Thomas Wood committed Feb 03, 2016 586 587 588 } @Article{Dawar2007Expressiveness,  Teresa Carbajo-Garcia committed Jun 15, 2017 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},  Thomas Wood committed Nov 03, 2017 596  month = feb,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 598  doi = {10.1016/j.ic.2006.10.006},  Teresa Carbajo-Garcia committed Jun 15, 2017 599 600  file = {Dawar2007Expressiveness.pdf:Dawar2007Expressiveness.pdf:PDF}, project = { TBD },  Thomas Wood committed Feb 03, 2016 601 602 603 } @InProceedings{Dawar2004Adjunct,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 608 609 610  editor = {Kamal Lodaya and Meena Mahajan}, volume = {3328}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 611  pages = {211--223},  Thomas Wood committed Nov 01, 2017 612  month = dec,  Teresa Carbajo-Garcia committed Sep 26, 2017 613  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 615  doi = {10.1007/978-3-540-30538-5_18},  Thomas Wood committed Nov 01, 2017 616  file = {Dawar2004Adjunct.pdf:Dawar2004Adjunct.pdf:PDF;:Dawar2004Adjunct.extended.pdf:PDF},  Teresa Carbajo-Garcia committed Jun 15, 2017 617  project = { TBD },  Thomas Wood committed Feb 03, 2016 618 619 620 } @InProceedings{Dinsdale-Young2013Views,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 625  editor = {Roberto Giacobazzi and Radhia Cousot},  Teresa Carbajo-Garcia committed Jun 15, 2017 626  pages = {287--300},  Thomas Wood committed Nov 24, 2017 627  month = jan,  Teresa Carbajo-Garcia committed Sep 26, 2017 628  publisher = {{ACM}},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 631  doi = {10.1145/2429069.2429104},  Teresa Carbajo-Garcia committed Jun 15, 2017 632  file = {Dinsdale-Young2013Views.pdf:Dinsdale-Young2013Views.pdf:PDF},  Thomas Wood committed Nov 24, 2017 633  project = {concurrency},  Thomas Wood committed Feb 03, 2016 634 635 636 } @InProceedings{Dinsdale-Young2010Concurrent,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 641 642 643  editor = {Theo D'Hondt}, volume = {6183}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 644  pages = {504--528},  Teresa Carbajo-Garcia committed Sep 26, 2017 645  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 647  doi = {10.1007/978-3-642-14107-2_24},  Teresa Carbajo-Garcia committed Jun 15, 2017 648 649  file = {Dinsdale-Young2010Concurrent.pdf:Dinsdale-Young2010Concurrent.pdf:PDF}, project = { concurrency },  Thomas Wood committed Feb 03, 2016 650 651 652 } @InProceedings{Dinsdale-Young2011Abstract,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 657 658 659  editor = {Andrea Corradini and Bartek Klin and Corina C{\^{\i}}rstea}, volume = {6859}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 660  pages = {36--39},  Teresa Carbajo-Garcia committed Sep 26, 2017 661  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 664  doi = {10.1007/978-3-642-22944-2_3},  Teresa Carbajo-Garcia committed Jun 15, 2017 665 666  file = {Dinsdale-Young2011Abstract.pdf:Dinsdale-Young2011Abstract.pdf:PDF}, project = { TBD },  Thomas Wood committed Feb 03, 2016 667 668 669 } @InProceedings{Dinsdale-Young2010Abstraction,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 674 675 676  editor = {Gary T. Leavens and Peter W. O'Hearn and Sriram K. Rajamani}, volume = {6217}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 677  pages = {199--215},  Teresa Carbajo-Garcia committed Sep 26, 2017 678  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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-levelfiction' of locality.},  Teresa Carbajo-Garcia committed Sep 26, 2017 680  doi = {10.1007/978-3-642-15057-9_14},  Thomas Wood committed Nov 24, 2017 681  file = {Dinsdale-Young2010Abstraction.pdf:Dinsdale-Young2010Abstraction.pdf:PDF;:Dinsdale-Young2010Abstraction.techreport.pdf:PDF},  Teresa Carbajo-Garcia committed Jun 15, 2017 682  project = { TBD },  Thomas Wood committed Feb 03, 2016 683 684 685 } @InProceedings{Gardner2010Reasoning,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 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}},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Feb 03, 2016 697 698 699 } @Article{Gardner2005Modelling,  Teresa Carbajo-Garcia committed Jun 15, 2017 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},  Thomas Wood committed Nov 03, 2017 707  month = sep,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 709  doi = {10.1016/j.tcs.2005.06.006},  Teresa Carbajo-Garcia committed Jun 15, 2017 710 711  file = {Gardner2005Modelling.pdf:Gardner2005Modelling.pdf:PDF}, project = { web },  Thomas Wood committed Feb 03, 2016 712 713 714 } @InProceedings{Gardner2003Modelling,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 719 720 721  editor = {Georg Lausen and Dan Suciu}, volume = {2921}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 722  pages = {130--146},  Thomas Wood committed Nov 03, 2017 723  month = sep,  Teresa Carbajo-Garcia committed Sep 26, 2017 724  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 725  abstract = {We introduce Xd$\pi$, a peer-to-peer model for reasoning about the dynamic behaviour of web  pmaksimo committed Feb 04, 2016 726  data. It is based on an idealised model of semi-structured data, and an extension of the pi-calculus with process  Thomas Wood committed Feb 03, 2016 727  mobility and with an operation for interacting with data. Our model can be used to reason about behaviour found  pmaksimo committed Feb 04, 2016 728  in, for example, dynamic web page programming, applet interaction, and service orchestration. We study  Teresa Carbajo-Garcia committed Jun 15, 2017 729  behavioural equivalences for Xd$\pi$, motivated by examples.},  Teresa Carbajo-Garcia committed Sep 26, 2017 730  doi = {10.1007/978-3-540-24607-7_9},  Teresa Carbajo-Garcia committed Jun 15, 2017 731 732  file = {Gardner2003Modelling.pdf:Gardner2003Modelling.pdf:PDF}, project = { web },  Thomas Wood committed Feb 03, 2016 733 734 735 } @InProceedings{Gardner2012Towards,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 740  editor = {John Field and Michael Hicks},  Teresa Carbajo-Garcia committed Jun 15, 2017 741  pages = {31--44},  Thomas Wood committed Nov 24, 2017 742  month = jan,  Teresa Carbajo-Garcia committed Sep 26, 2017 743  publisher = {{ACM}},  Teresa Carbajo-Garcia committed Jun 15, 2017 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.  Thomas Wood committed Nov 24, 2017 745   Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 747  doi = {10.1145/2103656.2103663},  Teresa Carbajo-Garcia committed Jun 15, 2017 748  file = {Gardner2012Towards.pdf:Gardner2012Towards.pdf:PDF},  Thomas Wood committed Nov 24, 2017 749  project = {web},  Thomas Wood committed Feb 03, 2016 750 751 752 } @InProceedings{Gardner2014Local,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 757 758 759  editor = {Zhong Shao}, volume = {8410}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 760  pages = {169--188},  Teresa Carbajo-Garcia committed Sep 26, 2017 761  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 763  doi = {10.1007/978-3-642-54833-8_10},  Teresa Carbajo-Garcia committed Jun 15, 2017 764 765  file = {Gardner2014Local.pdf:Gardner2014Local.pdf:PDF}, project = { concurrency },  Thomas Wood committed Feb 03, 2016 766 767 768 } @Article{Gardner2014Abstract,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 776  doi = {10.1016/j.entcs.2014.10.009},  Teresa Carbajo-Garcia committed Jun 15, 2017 777 778  file = {Gardner2014Abstract.pdf:Gardner2014Abstract.pdf:PDF}, project = { concurrency },  Thomas Wood committed Feb 03, 2016 779 780 781 } @InProceedings{Gardner2008DOM,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Feb 03, 2016 789 790 791 } @InProceedings{Gardner2008Local,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 796  editor = {Maurizio Lenzerini and Domenico Lembo},  Teresa Carbajo-Garcia committed Jun 15, 2017 797  pages = {261--270},  Teresa Carbajo-Garcia committed Sep 26, 2017 798  publisher = {{ACM}},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 800  doi = {10.1145/1376916.1376953},  Teresa Carbajo-Garcia committed Jun 15, 2017 801 802  file = {Gardner2008Local.pdf:Gardner2008Local.pdf:PDF}, project = { web },  Thomas Wood committed Feb 03, 2016 803 804 805 } @InProceedings{Gardner2009Small,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 810 811 812  editor = {Cosimo Laneve and Jianwen Su}, volume = {6194}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 813  pages = {178--195},  Teresa Carbajo-Garcia committed Sep 26, 2017 814  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 816  doi = {10.1007/978-3-642-14458-5_11},  Teresa Carbajo-Garcia committed Jun 15, 2017 817 818  file = {Gardner2009Small.pdf:Gardner2009Small.pdf:PDF}, project = { TBD },  Thomas Wood committed Feb 03, 2016 819 820 821 } @InProceedings{Maffeis2004Behavioural,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 826 827 828  editor = {Jean{-}Jacques L{\'{e}}vy and Ernst W. Mayr and John C. Mitchell}, volume = {155}, series = {{IFIP}},  Teresa Carbajo-Garcia committed Jun 15, 2017 829  pages = {535--548},  Thomas Wood committed Nov 03, 2017 830  month = aug,  Teresa Carbajo-Garcia committed Sep 26, 2017 831  publisher = {Kluwer/Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 833  doi = {10.1007/1-4020-8141-3_41},  Teresa Carbajo-Garcia committed Jun 15, 2017 834 835  file = {Maffeis2004Behavioural.pdf:Maffeis2004Behavioural.pdf:PDF}, project = { web },  Thomas Wood committed Feb 03, 2016 836 837 838 } @InProceedings{Ntzik2015Reasoning,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 843  editor = {Jonathan Aldrich and Patrick Eugster},  Teresa Carbajo-Garcia committed Jun 15, 2017 844 845  pages = {201--220}, month = oct,  Teresa Carbajo-Garcia committed Sep 26, 2017 846  publisher = {{ACM}},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 848  doi = {10.1145/2814270.2814306},  Teresa Carbajo-Garcia committed Jun 15, 2017 849 850  file = {Ntzik2015Reasoning.pdf:Ntzik2015Reasoning.pdf:PDF}, project = { concurrency },  Thomas Wood committed Feb 03, 2016 851 852 853 } @InProceedings{Ntzik2015Fault,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 858 859 860  editor = {Xinyu Feng and Sungwoo Park}, volume = {9458}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 861 862  pages = {169--188}, month = dec,  Teresa Carbajo-Garcia committed Sep 26, 2017 863  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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},  Teresa Carbajo-Garcia committed Jun 15, 2017 866  file = {Ntzik2015Fault.pdf:Ntzik2015Fault.pdf:PDF},  Teresa Carbajo-Garcia committed Jun 15, 2017 867  project = { concurrency },  Thomas Wood committed Feb 03, 2016 868 869 870 } @InProceedings{Raad2015CoLoSL,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 875 876 877  editor = {Jan Vitek}, volume = {9032}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 878  pages = {710--735},  Teresa Carbajo-Garcia committed Sep 26, 2017 879  publisher = {Springer},  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 881  doi = {10.1007/978-3-662-46669-8_29},  Teresa Carbajo-Garcia committed Jun 15, 2017 882 883  file = {Raad2015CoLoSL.pdf:Raad2015CoLoSL.pdf:PDF}, project = { concurrency },  Thomas Wood committed Feb 03, 2016 884 885 886 } @InProceedings{Raza2009Automatic,  Teresa Carbajo-Garcia committed Jun 15, 2017 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 committed Sep 26, 2017 891 892 893  editor = {Giuseppe Castagna}, volume = {5502}, series = {Lecture Notes in Computer Science},  Teresa Carbajo-Garcia committed Jun 15, 2017 894  pages = {348--362}, ` Teresa Carbajo-Garcia committed Sep 26, 2017