diff --git a/publications.bib b/publications.bib
index f97da6e82b84893bbd941854913836c6c4593986..829f8f6e1c2edf61524f8eac5dde1466e1ae305b 100644
--- a/publications.bib
+++ b/publications.bib
@@ -12,6 +12,707 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
project = { web },
}
+@InProceedings{Gardner2015Trusted,
+ author = {Philippa Gardner and Gareth Smith and Conrad Watt and Thomas Wood},
+ title = {{A Trusted Mechanised Specification of JavaScript: One Year On}},
+ booktitle = {Proceedings of the 27\textsuperscript{th} International Conference on Computer Aided Verification ({CAV'15})},
+ year = {2015},
+ pages = {3--10},
+ abstract = {The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL'14 and the current state of the project at CAV'15. We evaluate the work of POPL'14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google's V8 Array library, enabling us to cover more of the language and to pass more tests.},
+ file = {Gardner2015Trusted.pdf:Gardner2015Trusted.pdf:PDF},
+ project = { web },
+}
+
+@InProceedings{Gardner2007Introduction,
+ Title = {{An Introduction to Context Logic}},
+ Author = {Philippa Gardner and Uri Zarfaty},
+ Booktitle = {Proceedings of the 14\textsuperscript{th} International Workshop on Logic, Language, Information and Computation (WoLLIC'07)},
+ Year = {2007},
+ Pages = {189--202},
+
+ Project = { TBD },
+
+ Abstract = {This paper provides a gentle introduction to Context Logic. It contains work previously published with Calcagno [1,2], and is based on Gardner's notes for her course on Local Reasoning about Data Update at the Appsem PhD summer school [3] and Zarfaty's thesis [4].}
+}
+
+@InProceedings{daRochaPinto2015Steps,
+ author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner},
+ title = {{Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)}},
+ booktitle = {Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics ({MFPS'15})},
+ year = {2015},
+ pages = {3--18},
+ month = jun,
+ abstract = {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.},
+ doi = {10.1016/j.entcs.2015.12.002},
+ file = {daRochaPinto2015Steps.pdf:daRochaPinto2015Steps.pdf:PDF},
+ project = { concurrency },
+ url = {http://www.sciencedirect.com/science/article/pii/S1571066115000699},
+}
+
+@InProceedings{Raad2016DOM,
+ author = {Azalea Raad and Jos{\'{e}} {Fragoso Santos} and Philippa Gardner},
+ title = {{DOM:} Specification and Client Reasoning},
+ booktitle = {Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS'16)},
+ 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},
+ project = {concurrency},
+}
+
+@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},
+ project = { concurrency },
+}
+
+@PhdThesis{daRochaPinto2017Reasoning,
+ author = {Pedro {da Rocha Pinto}},
+ title = {Reasoning with Time and Data Abstractions},
+ school = {Imperial College London},
+ year = {2017},
+ 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},
+ project = { concurrency },
+}
+
+@PhdThesis{Raad2017Abstraction,
+ author = {Azalea Raad},
+ title = {Abstraction, Refinement and Concurrent Reasoning},
+ school = {Imperial College London},
+ year = {2017},
+ 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.},
+ 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.},
+ 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.},
+ file = {DOsualdo2017Deciding.pdf:DOsualdo2017Deciding.pdf:PDF},
+ project = {concurrency},
+}
+
+@InProceedings{DBLP:conf/cade/SantosGMN17,
+ author = {Jos{\'{e}} Fragoso Santos and Philippa Gardner and Petar Maksimovic and Daiva Naudziuniene},
+ title = {Towards Logic-Based Verification of JavaScript Programs},
+ booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
+ year = {2017},
+ editor = {Leonardo de Moura},
+ volume = {10395},
+ series = {Lecture Notes in Computer Science},
+ pages = {8--25},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/SantosGMN17},
+ doi = {10.1007/978-3-319-63046-5_2},
+ timestamp = {Wed, 12 Jul 2017 10:06:41 +0200},
+ url = {https://doi.org/10.1007/978-3-319-63046-5_2},
+}
+
+@InProceedings{DBLP:conf/aplas/RaadSG16,
+ author = {Azalea Raad and Jos{\'{e}} Fragoso Santos and Philippa Gardner},
+ title = {{DOM:} Specification and Client Reasoning},
+ booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
+ year = {2016},
+ editor = {Atsushi Igarashi},
+ volume = {10017},
+ series = {Lecture Notes in Computer Science},
+ pages = {401--422},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/aplas/RaadSG16},
+ doi = {10.1007/978-3-319-47958-3_21},
+ timestamp = {Fri, 19 May 2017 01:25:54 +0200},
+ url = {https://doi.org/10.1007/978-3-319-47958-3_21},
+}
+
+@Article{DBLP:journals/entcs/PintoDG15,
+ author = {Pedro da Rocha Pinto and Thomas Dinsdale{-}Young and Philippa Gardner},
+ title = {Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)},
+ journal = {Electr. Notes Theor. Comput. Sci.},
+ year = {2015},
+ volume = {319},
+ pages = {3--18},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/PintoDG15},
+ doi = {10.1016/j.entcs.2015.12.002},
+ timestamp = {Mon, 05 Jun 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.entcs.2015.12.002},
+}
+
+@InProceedings{DBLP:conf/cav/GardnerSWW15,
+ author = {Philippa Gardner and Gareth Smith and Conrad Watt and Thomas Wood},
+ title = {A Trusted Mechanised Specification of JavaScript: One Year On},
+ booktitle = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {I}},
+ year = {2015},
+ editor = {Daniel Kroening and Corina S. Pasareanu},
+ volume = {9206},
+ series = {Lecture Notes in Computer Science},
+ pages = {3--10},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/cav/GardnerSWW15},
+ doi = {10.1007/978-3-319-21690-4_1},
+ timestamp = {Thu, 01 Jun 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1007/978-3-319-21690-4_1},
+}
+
+@Article{DBLP:journals/dagstuhl-reports/BirkedalDGS15,
+ author = {Lars Birkedal and Derek Dreyer and Philippa Gardner and Zhong Shao},
+ title = {Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191)},
+ journal = {Dagstuhl Reports},
+ year = {2015},
+ volume = {5},
+ number = {5},
+ pages = {1--23},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/dagstuhl-reports/BirkedalDGS15},
+ doi = {10.4230/DagRep.5.5.1},
+ timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
+ url = {https://doi.org/10.4230/DagRep.5.5.1},
+}
+
+@InProceedings{DBLP:conf/popl/BodinCFGMNSS14,
+ author = {Martin Bodin and Arthur Chargu{\'{e}}raud and Daniele Filaretti and Philippa Gardner and Sergio Maffeis and Daiva Naudziuniene and Alan Schmitt and Gareth Smith},
+ title = {A trusted mechanised JavaSript specification},
+ booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014},
+ year = {2014},
+ editor = {Suresh Jagannathan and Peter Sewell},
+ pages = {87--100},
+ publisher = {{ACM}},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/BodinCFGMNSS14},
+ doi = {10.1145/2535838.2535876},
+ timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
+ url = {http://doi.acm.org/10.1145/2535838.2535876},
+}
+
+@Proceedings{DBLP:conf/esop/2013,
+ title = {Programming Languages and Systems - 22nd 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},
+ year = {2013},
+ editor = {Matthias Felleisen and Philippa Gardner},
+ volume = {7792},
+ series = {Lecture Notes in Computer Science},
+ publisher = {Springer},
+ isbn = {978-3-642-37035-9},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/2013},
+ doi = {10.1007/978-3-642-37036-6},
+ timestamp = {Fri, 19 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1007/978-3-642-37036-6},
+}
+
+@Article{DBLP:journals/tcs/CardelliG12,
+ author = {Luca Cardelli and Philippa Gardner},
+ title = {Processes in space},
+ journal = {Theor. Comput. Sci.},
+ year = {2012},
+ volume = {431},
+ pages = {40--55},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/CardelliG12},
+ doi = {10.1016/j.tcs.2011.12.051},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.tcs.2011.12.051},
+}
+
+@Article{DBLP:journals/sigmod/BenediktFGGMW10,
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/sigmod/BenediktFGGMW10},
+ doi = {10.1145/1860702.1860713},
+ timestamp = {Thu, 08 Jun 2017 01:00:00 +0200},
+ url = {http://doi.acm.org/10.1145/1860702.1860713},
+}
+
+@InProceedings{DBLP:conf/cie/CardelliG10,
+ author = {Luca Cardelli and Philippa Gardner},
+ title = {Processes in Space},
+ booktitle = {Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 - July 4, 2010. Proceedings},
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/cie/CardelliG10},
+ doi = {10.1007/978-3-642-13962-8_9},
+ timestamp = {Fri, 19 May 2017 01:26:07 +0200},
+ url = {https://doi.org/10.1007/978-3-642-13962-8_9},
+}
+
+@Article{DBLP:journals/entcs/CardelliCGKP09,
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/CardelliCGKP09},
+ doi = {10.1016/j.entcs.2009.02.009},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.entcs.2009.02.009},
+}
+
+@Article{DBLP:journals/tcs/CardelliCGKP09,
+ author = {Luca Cardelli and Emmanuelle Caron and Philippa Gardner and Ozan Kahramanogullari and Andrew Phillips},
+ title = {A process model of Rho GTP-binding proteins},
+ journal = {Theor. Comput. Sci.},
+ year = {2009},
+ volume = {410},
+ number = {33-34},
+ pages = {3166--3185},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/CardelliCGKP09},
+ doi = {10.1016/j.tcs.2009.04.029},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.tcs.2009.04.029},
+}
+
+@Proceedings{DBLP:conf/dbpl/2009,
+ title = {Database Programming Languages - {DBPL} 2009, 12th International Symposium, Lyon, France, August 24, 2009. Proceedings},
+ year = {2009},
+ editor = {Philippa Gardner and Floris Geerts},
+ volume = {5708},
+ series = {Lecture Notes in Computer Science},
+ publisher = {Springer},
+ isbn = {978-3-642-03792-4},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/dbpl/2009},
+ doi = {10.1007/978-3-642-03793-1},
+ timestamp = {Tue, 13 Jun 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1007/978-3-642-03793-1},
+}
+
+@Article{DBLP:journals/entcs/CardelliGK08,
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/CardelliGK08},
+ doi = {10.1016/j.entcs.2007.12.007},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.entcs.2007.12.007},
+}
+
+@Article{DBLP:journals/iandc/GardnerLW07,
+ author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
+ title = {Linear forwarders},
+ journal = {Inf. Comput.},
+ year = {2007},
+ volume = {205},
+ number = {10},
+ pages = {1526--1550},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/iandc/GardnerLW07},
+ doi = {10.1016/j.ic.2007.01.006},
+ timestamp = {Thu, 18 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.ic.2007.01.006},
+}
+
+@InProceedings{DBLP:conf/wollic/GardnerZ07,
+ author = {Philippa Gardner and Uri Zarfaty},
+ title = {An Introduction to Context Logic},
+ booktitle = {Logic, Language, Information and Computation, 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2-5, 2007, Proceedings},
+ year = {2007},
+ editor = {Daniel Leivant and Ruy J. G. B. de Queiroz},
+ volume = {4576},
+ series = {Lecture Notes in Computer Science},
+ pages = {189--202},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/wollic/GardnerZ07},
+ doi = {10.1007/978-3-540-73445-1_14},
+ timestamp = {Mon, 12 Jun 2017 16:41:07 +0200},
+ url = {https://doi.org/10.1007/978-3-540-73445-1_14},
+}
+
+@Article{DBLP:journals/entcs/ZarfatyG06,
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/ZarfatyG06},
+ doi = {10.1016/j.entcs.2006.04.020},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.entcs.2006.04.020},
+}
+
+@Article{DBLP:journals/tcs/GardnerY06,
+ author = {Philippa Gardner and Nobuko Yoshida},
+ title = {Editorial},
+ journal = {Theor. Comput. Sci.},
+ year = {2006},
+ volume = {358},
+ number = {2-3},
+ pages = {149},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/GardnerY06},
+ doi = {10.1016/j.tcs.2006.01.013},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.tcs.2006.01.013},
+}
+
+@Article{DBLP:journals/tcs/WischikG05,
+ author = {Lucian Wischik and Philippa Gardner},
+ title = {Explicit fusions},
+ journal = {Theor. Comput. Sci.},
+ year = {2005},
+ volume = {340},
+ number = {3},
+ pages = {606--630},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/WischikG05},
+ doi = {10.1016/j.tcs.2005.03.017},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/j.tcs.2005.03.017},
+}
+
+@Proceedings{DBLP:conf/dagstuhl/2004P4241,
+ title = {Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6.-11. June 2004},
+ year = {2005},
+ editor = {Barbara K{\"{o}}nig and Ugo Montanari and Philippa Gardner},
+ volume = {04241},
+ series = {Dagstuhl Seminar Proceedings},
+ publisher = {IBFI, Schloss Dagstuhl, Germany},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/dagstuhl/2004P4241},
+ timestamp = {Wed, 07 Jan 2015 00:00:00 +0100},
+ url = {http://drops.dagstuhl.de/portals/04241/},
+}
+
+@InProceedings{DBLP:conf/fossacs/WischikG04,
+ author = {Lucian Wischik and Philippa Gardner},
+ title = {Strong Bisimulation for the Explicit Fusion Calculus},
+ booktitle = {Foundations of Software Science and Computation Structures, 7th 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},
+ year = {2004},
+ editor = {Igor Walukiewicz},
+ volume = {2987},
+ series = {Lecture Notes in Computer Science},
+ pages = {484--498},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/fossacs/WischikG04},
+ doi = {10.1007/978-3-540-24727-2_34},
+ timestamp = {Mon, 29 May 2017 16:53:44 +0200},
+ url = {https://doi.org/10.1007/978-3-540-24727-2_34},
+}
+
+@Proceedings{DBLP:conf/concur/2004,
+ title = {{CONCUR} 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings},
+ year = {2004},
+ editor = {Philippa Gardner and Nobuko Yoshida},
+ volume = {3170},
+ series = {Lecture Notes in Computer Science},
+ publisher = {Springer},
+ isbn = {3-540-22940-X},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/concur/2004},
+ doi = {10.1007/b100113},
+ timestamp = {Tue, 30 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1007/b100113},
+}
+
+@InProceedings{DBLP:conf/dagstuhl/KonigMG04,
+ author = {Barbara K{\"{o}}nig and Ugo Montanari and Philippa Gardner},
+ title = {04241 Abstracts Collection - Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
+ booktitle = {Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6.-11. June 2004},
+ year = {2004},
+ editor = {Barbara K{\"{o}}nig and Ugo Montanari and Philippa Gardner},
+ volume = {04241},
+ series = {Dagstuhl Seminar Proceedings},
+ publisher = {IBFI, Schloss Dagstuhl, Germany},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/dagstuhl/KonigMG04},
+ timestamp = {Sun, 09 Jul 2017 01:00:00 +0200},
+ url = {http://drops.dagstuhl.de/opus/volltexte/2005/27},
+}
+
+@InProceedings{DBLP:conf/concur/GardnerLW03,
+ author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
+ title = {Linear Forwarders},
+ booktitle = {{CONCUR} 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings},
+ year = {2003},
+ editor = {Roberto M. Amadio and Denis Lugiez},
+ volume = {2761},
+ series = {Lecture Notes in Computer Science},
+ pages = {408--422},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/concur/GardnerLW03},
+ doi = {10.1007/978-3-540-45187-7_27},
+ timestamp = {Mon, 29 May 2017 16:53:44 +0200},
+ url = {https://doi.org/10.1007/978-3-540-45187-7_27},
+}
+
+@InProceedings{DBLP:conf/concur/GardnerLW02,
+ author = {Philippa Gardner and Cosimo Laneve and Lucian Wischik},
+ title = {The Fusion Machine},
+ booktitle = {{CONCUR} 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings},
+ 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},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/concur/GardnerLW02},
+ doi = {10.1007/3-540-45694-5_28},
+ timestamp = {Mon, 29 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1007/3-540-45694-5_28},
+}
+
+@InProceedings{DBLP:conf/concur/Gardner00,
+ author = {Philippa Gardner},
+ title = {From Process Calculi to Process Frameworks},
+ booktitle = {{CONCUR} 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings},
+ year = {2000},
+ editor = {Catuscia Palamidessi},
+ volume = {1877},
+ series = {Lecture Notes in Computer Science},
+ pages = {69--88},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/concur/Gardner00},
+ doi = {10.1007/3-540-44618-4_7},
+ timestamp = {Wed, 24 May 2017 15:40:44 +0200},
+ url = {https://doi.org/10.1007/3-540-44618-4_7},
+}
+
+@InProceedings{DBLP:conf/mfcs/GardnerW00,
+ author = {Philippa Gardner and Lucian Wischik},
+ title = {Explicit Fusions},
+ booktitle = {Mathematical Foundations of Computer Science 2000, 25th International Symposium, {MFCS} 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings},
+ year = {2000},
+ editor = {Mogens Nielsen and Branislav Rovan},
+ volume = {1893},
+ series = {Lecture Notes in Computer Science},
+ pages = {373--382},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/mfcs/GardnerW00},
+ doi = {10.1007/3-540-44612-5_33},
+ timestamp = {Wed, 24 May 2017 15:40:45 +0200},
+ url = {https://doi.org/10.1007/3-540-44612-5_33},
+}
+
+@Article{DBLP:journals/tcs/Gardner99,
+ author = {Philippa Gardner},
+ title = {Closed Action Calculi},
+ journal = {Theor. Comput. Sci.},
+ year = {1999},
+ volume = {228},
+ number = {1-2},
+ pages = {77--103},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/Gardner99},
+ doi = {10.1016/S0304-3975(98)00355-7},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/S0304-3975(98)00355-7},
+}
+
+@Article{DBLP:journals/entcs/Gardner97,
+ author = {Philippa Gardner},
+ title = {A Type-theoretic Description of Action Calculi},
+ journal = {Electr. Notes Theor. Comput. Sci.},
+ year = {1997},
+ volume = {10},
+ pages = {52},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/Gardner97},
+ doi = {10.1016/S1571-0661(05)82513-7},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/S1571-0661(05)82513-7},
+}
+
+@InProceedings{DBLP:conf/csl/BarberGHP97,
+ author = {Andrew G. Barber and Philippa Gardner and Masahito Hasegawa and Gordon D. Plotkin},
+ title = {From Action Calculi to Linear Logic},
+ booktitle = {Computer Science Logic, 11th International Workshop, {CSL} '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers},
+ year = {1997},
+ editor = {Mogens Nielsen and Wolfgang Thomas},
+ volume = {1414},
+ series = {Lecture Notes in Computer Science},
+ pages = {78--97},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/csl/BarberGHP97},
+ doi = {10.1007/BFb0028008},
+ timestamp = {Tue, 23 May 2017 11:53:58 +0200},
+ url = {https://doi.org/10.1007/BFb0028008},
+}
+
+@InProceedings{DBLP:conf/tacs/GardnerH97,
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/tacs/GardnerH97},
+ doi = {10.1007/BFb0014569},
+ timestamp = {Mon, 22 May 2017 17:11:16 +0200},
+ url = {https://doi.org/10.1007/BFb0014569},
+}
+
+@Article{DBLP:journals/entcs/Gardner95,
+ author = {Philippa Gardner},
+ title = {A name-free account of action calculi},
+ journal = {Electr. Notes Theor. Comput. Sci.},
+ year = {1995},
+ volume = {1},
+ pages = {214--231},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/Gardner95},
+ doi = {10.1016/S1571-0661(04)80012-4},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1016/S1571-0661(04)80012-4},
+}
+
+@Article{DBLP:journals/mscs/Gardner95,
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/mscs/Gardner95},
+ doi = {10.1017/S0960129500000785},
+ timestamp = {Sun, 28 May 2017 01:00:00 +0200},
+ url = {https://doi.org/10.1017/S0960129500000785},
+}
+
+@InProceedings{DBLP:conf/tacs/Gardner94,
+ 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},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/tacs/Gardner94},
+ doi = {10.1007/3-540-57887-0_115},
+ timestamp = {Sat, 20 May 2017 15:32:50 +0200},
+ url = {https://doi.org/10.1007/3-540-57887-0_115},
+}
+
+@InProceedings{DBLP:conf/lpar/Gardner93,
+ author = {Philippa Gardner},
+ title = {A New Type THeory for Representing Logics},
+ booktitle = {Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings},
+ year = {1993},
+ editor = {Andrei Voronkov},
+ volume = {698},
+ series = {Lecture Notes in Computer Science},
+ pages = {146--157},
+ publisher = {Springer},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/lpar/Gardner93},
+ doi = {10.1007/3-540-56944-8_49},
+ timestamp = {Sat, 20 May 2017 15:32:54 +0200},
+ url = {https://doi.org/10.1007/3-540-56944-8_49},
+}
+
+@PhdThesis{DBLP:phd/ethos/Gardner92,
+ author = {Philippa Gardner},
+ title = {Representing logics in type theory},
+ school = {University of Edinburgh, {UK}},
+ year = {1992},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/phd/ethos/Gardner92},
+ timestamp = {Thu, 06 Oct 2016 01:00:00 +0200},
+ url = {http://hdl.handle.net/1842/14888},
+}
+
@Article{Calcagno2010Adjunct,
author = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
title = {{Adjunct elimination in Context Logic for Trees}},
@@ -21,6 +722,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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.},
+ doi = {10.1016/j.ic.2009.02.013},
file = {Calcagno2010Adjunct.pdf:Calcagno2010Adjunct.pdf:PDF},
project = { TBD },
}
@@ -30,8 +732,13 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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},
+ editor = {Zhong Shao},
+ volume = {4807},
+ series = {Lecture Notes in Computer Science},
pages = {255--270},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-540-76637-7_17},
file = {Calcagno2007Adjunct.pdf:Calcagno2007Adjunct.pdf:PDF},
project = { TBD },
}
@@ -41,8 +748,15 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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},
+ editor = {Vladimiro Sassone},
+ volume = {3441},
+ series = {Lecture Notes in Computer Science},
pages = {395--409},
+ publisher = {Springer},
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.},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/fossacs/CalcagnoGH05},
+ doi = {10.1007/978-3-540-31982-5_25},
file = {Calcagno2005From.pdf:Calcagno2005Separation.pdf:PDF},
project = { TBD },
}
@@ -52,10 +766,14 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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},
+ editor = {Martin Hofmann and Matthias Felleisen},
pages = {123--134},
+ publisher = {{ACM}},
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.},
+ doi = {10.1145/1190216.1190236},
file = {Calcagno2007Context.pdf:Calcagno2007Context.pdf:PDF},
project = { TBD },
+ url = {http://doi.acm.org/10.1145/1190216.1190236},
}
@Article{Calcagno2007Local,
@@ -66,6 +784,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
volume = {172},
pages = {133--175},
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.},
+ doi = {10.1016/j.entcs.2007.02.006},
file = {Calcagno2007Local.pdf:Calcagno2007Local.pdf:PDF},
project = { TBD },
}
@@ -75,10 +794,16 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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},
+ editor = {Jens Palsberg and Mart{\'{\i}}n Abadi},
pages = {271--282},
+ publisher = {{ACM}},
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.},
+ bibsource = {dblp computer science bibliography, http://dblp.org},
+ doi = {10.1145/1040305.1040328},
file = {Calcagno2005Context.pdf:Calcagno2005Context.pdf:PDF},
project = { TBD },
+ timestamp = {Tue, 22 May 2012 15:24:56 +0200},
+ url = {http://doi.acm.org/10.1145/1040305.1040328},
}
@Article{Cardelli2007Manipulating,
@@ -99,22 +824,31 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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},
+ editor = {Andrew D. Gordon},
+ volume = {2620},
+ series = {Lecture Notes in Computer Science},
pages = {216--232},
+ publisher = {Springer},
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.1007/3-540-36576-1_14},
file = {Cardelli2003Manipulating.pdf:Cardelli2003Manipulating.pdf:PDF},
project = { TBD },
}
@InProceedings{Cardelli2002Spatial,
- Title = {{A Spatial Logic for Querying Graphs}},
- Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
- Booktitle = {Proceedings of the 29\textsuperscript{th} International Colloquium on Automata, Languages and Programming ({ICALP'02})},
- Year = {2002},
- Pages = {597--610},
-
- Project = { TBD },
-
- 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.}
+ 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},
+ 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},
+ project = { TBD },
+ url = {https://doi.org/10.1007/3-540-45465-9_51},
}
@Article{Dawar2007Expressiveness,
@@ -126,6 +860,7 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
number = {3},
pages = {263--310},
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.},
+ doi = {10.1016/j.ic.2006.10.006},
file = {Dawar2007Expressiveness.pdf:Dawar2007Expressiveness.pdf:PDF},
project = { TBD },
}
@@ -135,8 +870,13 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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},
+ editor = {Kamal Lodaya and Meena Mahajan},
+ volume = {3328},
+ series = {Lecture Notes in Computer Science},
pages = {211--223},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-540-30538-5_18},
file = {Dawar2004Adjunct.pdf:Dawar2004Adjunct.pdf:PDF},
project = { TBD },
}
@@ -146,9 +886,12 @@ We present JSCert, a formalisation of the current ECMA standard in the Coq proof
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},
+ editor = {Roberto Giacobazzi and Radhia Cousot},
pages = {287--300},
+ publisher = {{ACM}},
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.},
+ doi = {10.1145/2429069.2429104},
file = {Dinsdale-Young2013Views.pdf:Dinsdale-Young2013Views.pdf:PDF},
project = { concurrency },
}
@@ -158,8 +901,13 @@ In this paper, we present the 'Concurrent Views Framework', a metatheory of conc
title = {{Concurrent Abstract Predicates}},
booktitle = {Proceedings of the 24\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP'10})},
year = {2010},
+ editor = {Theo D'Hondt},
+ volume = {6183},
+ series = {Lecture Notes in Computer Science},
pages = {504--528},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-642-14107-2_24},
file = {Dinsdale-Young2010Concurrent.pdf:Dinsdale-Young2010Concurrent.pdf:PDF},
project = { concurrency },
}
@@ -169,9 +917,14 @@ In this paper, we present the 'Concurrent Views Framework', a metatheory of conc
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},
+ editor = {Andrea Corradini and Bartek Klin and Corina C{\^{\i}}rstea},
+ volume = {6859},
+ series = {Lecture Notes in Computer Science},
pages = {36--39},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-642-22944-2_3},
file = {Dinsdale-Young2011Abstract.pdf:Dinsdale-Young2011Abstract.pdf:PDF},
project = { TBD },
}
@@ -181,8 +934,13 @@ throughout the proof.},
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},
+ editor = {Gary T. Leavens and Peter W. O'Hearn and Sriram K. Rajamani},
+ volume = {6217},
+ series = {Lecture Notes in Computer Science},
pages = {199--215},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-642-15057-9_14},
file = {Dinsdale-Young2010Abstraction.pdf:Dinsdale-Young2010Abstraction.pdf:PDF},
project = { TBD },
}
@@ -192,6 +950,9 @@ throughout the proof.},
title = {{Reasoning About Client-side Web Programs: Invited Talk}},
booktitle = {Proceedings of the 2010 {EDBT/ICDT} Workshops},
year = {2010},
+ 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}},
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},
@@ -207,6 +968,7 @@ throughout the proof.},
number = {1},
pages = {104--131},
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.},
+ doi = {10.1016/j.tcs.2005.06.006},
file = {Gardner2005Modelling.pdf:Gardner2005Modelling.pdf:PDF},
project = { web },
}
@@ -216,12 +978,17 @@ throughout the proof.},
title = {{Modelling Dynamic Web Data}},
booktitle = {Proceedings of 9\textsuperscript{th} International Workshop on Database Programming Languages ({DBPL'03})},
year = {2003},
+ editor = {Georg Lausen and Dan Suciu},
+ volume = {2921},
+ series = {Lecture Notes in Computer Science},
pages = {130--146},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-540-24607-7_9},
file = {Gardner2003Modelling.pdf:Gardner2003Modelling.pdf:PDF},
project = { web },
}
@@ -231,9 +998,12 @@ throughout the proof.},
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},
+ editor = {John Field and Michael Hicks},
pages = {31--44},
+ publisher = {{ACM}},
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.
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.},
+ doi = {10.1145/2103656.2103663},
file = {Gardner2012Towards.pdf:Gardner2012Towards.pdf:PDF},
project = { web },
}
@@ -243,8 +1013,13 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
title = {{Local Reasoning for the {POSIX} File System}},
booktitle = {Proceedings of the 23\textsuperscript{rd} European Symposium on Programming ({ESOP'14})},
year = {2014},
+ editor = {Zhong Shao},
+ volume = {8410},
+ series = {Lecture Notes in Computer Science},
pages = {169--188},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-642-54833-8_10},
file = {Gardner2014Local.pdf:Gardner2014Local.pdf:PDF},
project = { concurrency },
}
@@ -257,21 +1032,11 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
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.},
+ doi = {10.1016/j.entcs.2014.10.009},
file = {Gardner2014Abstract.pdf:Gardner2014Abstract.pdf:PDF},
project = { concurrency },
}
-@InProceedings{Gardner2015Trusted,
- author = {Philippa Gardner and Gareth Smith and Conrad Watt and Thomas Wood},
- title = {{A Trusted Mechanised Specification of JavaScript: One Year On}},
- booktitle = {Proceedings of the 27\textsuperscript{th} International Conference on Computer Aided Verification ({CAV'15})},
- year = {2015},
- pages = {3--10},
- abstract = {The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL'14 and the current state of the project at CAV'15. We evaluate the work of POPL'14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google's V8 Array library, enabling us to cover more of the language and to pass more tests.},
- file = {Gardner2015Trusted.pdf:Gardner2015Trusted.pdf:PDF},
- project = { web },
-}
-
@InProceedings{Gardner2008DOM,
author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
title = {{DOM: Towards a Formal Specification}},
@@ -287,8 +1052,11 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
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},
+ editor = {Maurizio Lenzerini and Domenico Lembo},
pages = {261--270},
+ publisher = {{ACM}},
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.},
+ doi = {10.1145/1376916.1376953},
file = {Gardner2008Local.pdf:Gardner2008Local.pdf:PDF},
project = { web },
}
@@ -298,24 +1066,17 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
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},
+ editor = {Cosimo Laneve and Jianwen Su},
+ volume = {6194},
+ series = {Lecture Notes in Computer Science},
pages = {178--195},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-642-14458-5_11},
file = {Gardner2009Small.pdf:Gardner2009Small.pdf:PDF},
project = { TBD },
}
-@InProceedings{Gardner2007Introduction,
- Title = {{An Introduction to Context Logic}},
- Author = {Philippa Gardner and Uri Zarfaty},
- Booktitle = {Proceedings of the 14\textsuperscript{th} International Workshop on Logic, Language, Information and Computation (WoLLIC'07)},
- Year = {2007},
- Pages = {189--202},
-
- Project = { TBD },
-
- Abstract = {This paper provides a gentle introduction to Context Logic. It contains work previously published with Calcagno [1,2], and is based on Gardner's notes for her course on Local Reasoning about Data Update at the Appsem PhD summer school [3] and Zarfaty's thesis [4].}
-}
-
@Article{Maffeis2008Behavioural,
author = {Sergio Maffeis and Philippa Gardner},
title = {{Behavioural Equivalences for Dynamic Web Data}},
@@ -325,6 +1086,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
number = {1},
pages = {86--138},
abstract = {We study behavioural equivalences for dynamic web data in Xdn, a model for reasoning about behaviour found in (for example) dynamic web page programming, applet interaction, and web-service orchestration. Xdn 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. },
+ doi = {10.1016/j.jlap.2007.06.004},
file = {Maffeis2008Behavioural.pdf:Maffeis2008Behavioural.pdf:PDF},
project = { web },
}
@@ -334,8 +1096,13 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
title = {{Behavioural Equivalences for Dynamic Web Data}},
booktitle = {Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {(TCS'04)}},
year = {2004},
+ editor = {Jean{-}Jacques L{\'{e}}vy and Ernst W. Mayr and John C. Mitchell},
+ volume = {155},
+ series = {{IFIP}},
pages = {535--548},
+ publisher = {Kluwer/Springer},
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.},
+ doi = {10.1007/1-4020-8141-3_41},
file = {Maffeis2004Behavioural.pdf:Maffeis2004Behavioural.pdf:PDF},
project = { web },
}
@@ -345,9 +1112,12 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
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},
+ editor = {Jonathan Aldrich and Patrick Eugster},
pages = {201--220},
month = oct,
+ publisher = {{ACM}},
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.},
+ doi = {10.1145/2814270.2814306},
file = {Ntzik2015Reasoning.pdf:Ntzik2015Reasoning.pdf:PDF},
project = { concurrency },
}
@@ -357,8 +1127,12 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
title = {{Fault-tolerant Resource Reasoning}},
booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS'15})},
year = {2015},
+ editor = {Xinyu Feng and Sungwoo Park},
+ volume = {9458},
+ series = {Lecture Notes in Computer Science},
pages = {169--188},
month = dec,
+ publisher = {Springer},
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},
file = {Ntzik2015Fault.pdf:Ntzik2015Fault.pdf:PDF},
@@ -370,8 +1144,13 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
title = {{CoLoSL: Concurrent Local Subjective Logic}},
booktitle = {Proceedings of the 24\textsuperscript{th} European Symposium on Programming ({ESOP'15})},
year = {2015},
+ editor = {Jan Vitek},
+ volume = {9032},
+ series = {Lecture Notes in Computer Science},
pages = {710--735},
+ publisher = {Springer},
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.},
+ doi = {10.1007/978-3-662-46669-8_29},
file = {Raad2015CoLoSL.pdf:Raad2015CoLoSL.pdf:PDF},
project = { concurrency },
}
@@ -381,8 +1160,13 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
title = {{Automatic Parallelization with Separation Logic}},
booktitle = {Proceedings of the 18\textsuperscript{th} European Symposium on Programming ({ESOP'09})},
year = {2009},
+ editor = {Giuseppe Castagna},
+ volume = {5502},
+ series = {Lecture Notes in Computer Science},
pages = {348--362},
+ publisher = {Springer},
abstract = {We present a separation logic framework which can express properties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.},
+ doi = {10.1007/978-3-642-00590-9_25},
file = {Raza2009Automatic.pdf:Raza2009Automatic.pdf:PDF},
project = { concurrency },
}
@@ -398,7 +1182,6 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
doi = {10.2168/LMCS-5(2:4)2009},
file = {Raza2009Footprints.pdf:Raza2009Footprints.pdf:PDF},
project = { concurrency },
- url = {https://arxiv.org/abs/0903.1032},
}
@InProceedings{Raza2008Footprints,
@@ -406,8 +1189,13 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
title = {{Footprints in Local Reasoning}},
booktitle = {Proceedings of the 11\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS'08})},
year = {2008},
+ editor = {Roberto M. Amadio},
+ volume = {4962},
+ series = {Lecture Notes in Computer Science},
pages = {201--215},
+ publisher = {Springer},
abstract = {We present a separation logic framework which can express properties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.},
+ doi = {10.1007/978-3-540-78499-9_15},
file = {Raza2008Footprints.pdf:Raza2008Footprints.pdf:PDF},
project = { concurrency },
}
@@ -417,8 +1205,10 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
title = {{A Simple Abstraction for Complex Concurrent Indexes}},
booktitle = {Proceedings of the 26\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA'11})},
year = {2011},
+ editor = {Cristina Videira Lopes and Kathleen Fisher},
pages = {845--864},
month = oct,
+ publisher = {{ACM}},
abstract = {Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is insufficient for reasoning about indexes that are accessed concurrently.
We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, however, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and B-Link trees. The complexity of these algorithms, in particular the B-Link tree algorithm, can be completely hidden from the client's view by our abstract specification.},
doi = {10.1145/2048066.2048131},
@@ -431,8 +1221,12 @@ We present an abstract specification for concurrent indexes. We verify several r
title = {{TaDA: A Logic for Time and Data Abstraction}},
booktitle = {Proceedings of the 28\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP'14})},
year = {2014},
+ editor = {Richard E. Jones},
+ volume = {8586},
+ series = {Lecture Notes in Computer Science},
pages = {207--231},
month = jul,
+ publisher = {Springer},
abstract = {To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.
Building on separation logic with concurrent abstract predicates (CAP), we introduce TaDA, a program logic which combines the benefits of abstract atomicity and abstract disjointness. We give several examples: an atomic lock module, a CAP example with a twist, which cannot be done using linearisability; an atomic MCAS module implemented using our lock module, a classic linearisability example which cannot be done using CAP; and a double-ended queue module implemented using MCAS.},
doi = {10.1007/978-3-662-44202-9_9},
@@ -440,27 +1234,17 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
project = { concurrency, tada },
}
-@InProceedings{daRochaPinto2015Steps,
- author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner},
- title = {{Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)}},
- booktitle = {Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics ({MFPS'15})},
- year = {2015},
- pages = {3--18},
- month = jun,
- abstract = {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.},
- doi = {10.1016/j.entcs.2015.12.002},
- file = {daRochaPinto2015Steps.pdf:daRochaPinto2015Steps.pdf:PDF},
- project = { concurrency },
- url = {http://www.sciencedirect.com/science/article/pii/S1571066115000699},
-}
-
@InProceedings{daRochaPinto2016Modular,
author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner and Julian Sutherland},
title = {Modular Termination Verification for Non-blocking Concurrency},
booktitle = {Proceedings of the 25\textsuperscript{th} European Symposium on Programming ({ESOP'16})},
year = {2016},
+ editor = {Peter Thiemann},
+ volume = {9632},
+ series = {Lecture Notes in Computer Science},
pages = {176--201},
month = apr,
+ publisher = {Springer},
abstract = {We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread's concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.},
doi = {10.1007/978-3-662-49498-1_8},
file = {daRochaPinto2016Modular.techreport.pdf:daRochaPinto2016Modular.techreport.pdf:PDF;daRochaPinto2016Modular.pdf:daRochaPinto2016Modular.pdf:PDF},
@@ -472,6 +1256,9 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
title = {Verifying Concurrent Graph Algorithms},
booktitle = {Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS'16)},
year = {2016},
+ editor = {Atsushi Igarashi},
+ volume = {10017},
+ series = {Lecture Notes in Computer Science},
pages = {314--334},
abstract = {We show how to verify four challenging concurrent finegrained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction (CoLoSL) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.},
doi = {10.1007/978-3-319-47958-3_17},
@@ -479,127 +1266,23 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
project = {concurrency},
}
-@InProceedings{Raad2016DOM,
- author = {Azalea Raad and Jos{\'{e}} {Fragoso Santos} and Philippa Gardner},
- title = {{DOM:} Specification and Client Reasoning},
- booktitle = {Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS'16)},
- 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},
- project = {concurrency},
-}
-
@InProceedings{Xiong2017Abstract,
author = {Shale Xiong and Pedro {da Rocha Pinto} and Gian Ntzik and Philippa Gardner},
title = {Abstract Specifications for Concurrent Maps},
booktitle = {Proceedings of the 26\textsuperscript{th} European Symposium on Programming ({ESOP'17})},
year = {2017},
+ editor = {Hongseok Yang},
+ volume = {10201},
+ series = {Lecture Notes in Computer Science},
pages = {964--990},
month = apr,
+ publisher = {Springer},
abstract = {Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.},
doi = {10.1007/978-3-662-54434-1_36},
file = {Xiong2017Abstract.techreport.pdf:Xiong2017Abstract.techreport.pdf:PDF;Xiong2017Abstract.pdf:Xiong2017Abstract.pdf:PDF},
project = { concurrency, tada },
}
-@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},
- project = { concurrency },
-}
-
-@PhdThesis{daRochaPinto2017Reasoning,
- author = {Pedro {da Rocha Pinto}},
- title = {Reasoning with Time and Data Abstractions},
- school = {Imperial College London},
- year = {2017},
- 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},
- project = { concurrency },
-}
-
-@PhdThesis{Raad2017Abstraction,
- author = {Azalea Raad},
- title = {Abstraction, Refinement and Concurrent Reasoning},
- school = {Imperial College London},
- year = {2017},
- 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.},
- 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.},
- 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.},
- file = {DOsualdo2017Deciding.pdf:DOsualdo2017Deciding.pdf:PDF},
- project = {concurrency},
-}
-
@Comment{jabref-meta: databaseType:bibtex;}
@Comment{jabref-meta: saveActions:enabled;