diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4db4e1b5095eaa5157bd4780c5c9684ede475f6d..d154622224dbae4835ee1b0967f02917df4e3c95 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,24 +1,55 @@
-before_script:
+stages:
+ - update
+ - test
+ - deploy
+
+update_publications:
+ stage: update
+ script:
+ - git checkout -B ${CI_BUILD_REF_NAME}
+ - git submodule update --init --remote
+ - git add publications
+ - git commit -m "[AUTO] Updating publications submodule" --author="Resource Reasoning Group Backup Bot <rr-gitlab-bot@example.com>" || exit 0
+ - git remote rm rw || exit 0
+ - git remote add rw git@gitlab.doc.ic.ac.uk:${CI_PROJECT_PATH}.git
+ - eval `ssh-agent`
+ - echo "$PUSH_KEY" | ssh-add -
+ - git push rw ${CI_BUILD_REF_NAME}
+ - ssh-agent -k
+ only:
+ - triggers
+
+.before_script: &before_script
- bundle install --without=development
+ - bundle exec rake init
test:
stage: test
+ before_script: *before_script
script:
- bundle exec rake test
-
-# Not a test stage to prevent race conditions with gem installations.
-deadlinks:
- stage: deploy
- script:
- - bundle exec rake testlinks
- allow_failure: true
+ except:
+ - triggers
deploy:
stage: deploy
environment: production
+ before_script: *before_script
script:
- bundle exec rake deploy
tags:
- doc
only:
- master
+ except:
+ - triggers
+
+# Not a test stage to prevent race conditions with gem installations.
+deadlinks:
+ stage: deploy
+ script:
+ - bundle exec rake testlinks
+ allow_failure: true
+ except:
+ - triggers
+
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000000000000000000000000000000000000..0a24756af9262f952f1eadd36b5a0998de2bac00
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,4 @@
+[submodule "publications"]
+ path = publications
+ url = https://gitlab.doc.ic.ac.uk/resource-reasoning/publications.git
+ branch = master
diff --git a/Gemfile b/Gemfile
index 5a1aa47e037952f68e2f4e28c3826ee064ce0c29..9e3f083be3fe235e0ce5493bd0c0b93284767d7f 100644
--- a/Gemfile
+++ b/Gemfile
@@ -15,5 +15,4 @@ group :test do
end
group :development do
- gem 'pry'
end
diff --git a/Gemfile.lock b/Gemfile.lock
index 6eebea0c412eff4c8449cf59bc5652e542563ec5..57cf9d6b3b38b6335eb83a19cb36e01e63182388 100644
--- a/Gemfile.lock
+++ b/Gemfile.lock
@@ -6,7 +6,7 @@ GEM
i18n (~> 0.7)
minitest (~> 5.1)
tzinfo (~> 1.1)
- addressable (2.5.0)
+ addressable (2.5.1)
public_suffix (~> 2.0, >= 2.0.2)
bibtex-ruby (4.4.3)
latex-decode (~> 0.0)
@@ -15,7 +15,6 @@ GEM
citeproc-ruby (1.1.6)
citeproc (>= 1.0.4, < 2.0)
csl (~> 1.4)
- coderay (1.1.1)
colorator (1.1.0)
colored (1.2)
concurrent-ruby (1.0.5)
@@ -69,7 +68,6 @@ GEM
rb-fsevent (~> 0.9, >= 0.9.4)
rb-inotify (~> 0.9, >= 0.9.7)
mercenary (0.3.6)
- method_source (0.8.2)
mini_portile2 (2.1.0)
minitest (5.10.1)
namae (0.11.3)
@@ -78,10 +76,6 @@ GEM
parallel (1.11.1)
pathutil (0.14.0)
forwardable-extended (~> 2.6)
- pry (0.10.4)
- coderay (~> 1.1.0)
- method_source (~> 0.8.1)
- slop (~> 3.4)
public_suffix (2.0.5)
rake (12.0.0)
rb-fsevent (0.9.8)
@@ -90,11 +84,10 @@ GEM
rouge (1.11.1)
safe_yaml (1.0.4)
sass (3.4.23)
- slop (3.6.0)
thread_safe (0.3.6)
typhoeus (0.8.0)
ethon (>= 0.8.0)
- tzinfo (1.2.2)
+ tzinfo (1.2.3)
thread_safe (~> 0.1)
unicode (0.4.4.2)
yell (2.0.7)
@@ -108,7 +101,6 @@ DEPENDENCIES
jekyll-redirect-from
jekyll-scholar (~> 5.9.1)
jekyll-sitemap
- pry
rake
BUNDLED WITH
diff --git a/README.md b/README.md
index fc9cd18c92061d24922f86780c0c58abcc39ef7a..df08fe073ce7242b921b91d6947306482cb3e348 100644
--- a/README.md
+++ b/README.md
@@ -13,34 +13,10 @@ you should have access to edit it if a member of the resource-reasoning group.
[](https://gitlab.doc.ic.ac.uk/resource-reasoning/psvg.doc.ic.ac.uk/commits/master)
[](https://gemnasium.com/6ba7afbbfda9adcba06f007cc565a29a)
-Managing Content
-----------------
-
+## Managing Content
### Publications
-
-#### File Downloads
-Files associated with publications should be placed in the `publications` directory.
-The filename prefix *must* be the key used for the corresponding entry in the BibTeX file.
-The filename suffix (extension) determines how the file appears in the page listing. Unknown filetypes are permitted,
-but will be printed in a bland, not-very-descriptive way.
-
-Known filename suffixes are defined in `_data/publication_file_types.yml` and are summarised in the table below:
-
-<style>
-td, th { padding: 3px; }
-td i { text-align: center; }
-</style>
-<table>
- <tr><th>Extension</th><th>Icon</th><th>Text</th><th>File contents used as link?</th></tr>
-{% for type in site.data.publication_file_types %}
- <tr>
- <td><code class="highligher-rouge">.{{ type.ext }}</code></td>
- <td style="text-align: center"><i class="fa {{ type.icon }}"></i></td>
- <td>{{ type.text }}</td>
- <td style="text-align: center"><i class="fa fa-{% if type.include %}check{% else %}times{% endif %}"></i></td>
- </tr>
-{% endfor %}
-</table>
+Please see [the dedicated publications repository](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications) for
+instructions on how to add new publications to the website.
Technical Detail
----------------
@@ -96,6 +72,7 @@ If you wish to test the site locally, ensure you have ruby installed, and then i
```
gem install bundler
bundle install
+bundle exec rake init
```
And to start a local webserver that remakes files whenever changed:
diff --git a/Rakefile b/Rakefile
index d46d825dc17562ca454132c9abccb7aff46ccf04..b8d7ec54325dabcbbdcdd168c7fb4af501aa2da0 100644
--- a/Rakefile
+++ b/Rakefile
@@ -2,6 +2,11 @@ require 'html-proofer'
task :default => :build
+desc "Initialise/update git submodules"
+task :init do
+ sh "git submodule update --init --remote"
+end
+
desc "Build the site"
task :build do
sh "bundle exec jekyll build"
@@ -10,7 +15,7 @@ end
htmlproofer_config = {
:disable_external => true,
:check_html => true,
- :parallel => { :in_processes => 4 }
+ :parallel => { :in_processes => 1 }
}
desc "Build the site and test output for dead links, invalid html etc."
diff --git a/_data/publication_file_types.yml b/_data/publication_file_types.yml
deleted file mode 100644
index 1e28fa5f9b87565d3b1cf4981c3c7e5e55b823fe..0000000000000000000000000000000000000000
--- a/_data/publication_file_types.yml
+++ /dev/null
@@ -1,25 +0,0 @@
-# This file defines how particular supplementary file types should be rendered
-# on a publication page.
-
-# Fields:
-# ext: the file extension (longest part)
-# icon: fontawesome identifier names (see http://fontawesome.io/icons/)
-# text: descriptive text for type of file
-# include: set to true to use the *contents* of the file as the URL to link to
-- ext: pdf
- icon: fa-file-text-o
- text: "Authors' Preprint"
-- ext: techreport.pdf
- icon: fa-file-text-o
- text: Technical Report
-- ext: zip
- icon: fa-file-archive-o
- text: "File Archive (.zip)"
-- ext: github.link
- icon: fa-github
- text: Code Repository (GitHub)
- include: true
-- ext: repo.link
- icon: fa-code-fork
- text: Code Repository
- include: true
diff --git a/_data/publication_file_types.yml b/_data/publication_file_types.yml
new file mode 120000
index 0000000000000000000000000000000000000000..2e64806d556fe1157d3d75009093795250085645
--- /dev/null
+++ b/_data/publication_file_types.yml
@@ -0,0 +1 @@
+../publications/_publication_file_types.yml
\ No newline at end of file
diff --git a/publications b/publications
new file mode 160000
index 0000000000000000000000000000000000000000..4553e4ef5241df298fd4355dac23ef08bd974f9b
--- /dev/null
+++ b/publications
@@ -0,0 +1 @@
+Subproject commit 4553e4ef5241df298fd4355dac23ef08bd974f9b
diff --git a/publications/README.md b/publications/README.md
deleted file mode 100644
index 95081b99a4a877801e57f807a9c8ce8e04950e58..0000000000000000000000000000000000000000
--- a/publications/README.md
+++ /dev/null
@@ -1,17 +0,0 @@
-Paper Downloads
-===============
-
-Papers and supporting supplementary material should be placed in this directory.
-
-Check with the publisher's T&Cs to determine which version of the paper you are allowed to publish here. Often it is
-only the pre-print edition that is passed to the publisher **before** they make any changes. The final proof copy and
-the publisher's own copy is often not permitted to be published.
-
-The paper should also be deposited into [Imperial Spiral](http://spiral.imperial.ac.uk/).
-
-Files should be named by their key in the publications BibTeX file, suffixed with the appropriate extension.
-
-Technical reports should be named as ***bibtex_key***.techreport.***ext***
-
-Additional file types are also supportable, see [the README in the website root (as published
-online)](https://psvg.doc.ic.ac.uk/README.html) for the full list.
diff --git a/publications/publications.bib b/publications/publications.bib
deleted file mode 100644
index 13b895a52bae9790b3098f8057269735d57a60d9..0000000000000000000000000000000000000000
--- a/publications/publications.bib
+++ /dev/null
@@ -1,575 +0,0 @@
-% This file was created with JabRef 2.10.
-% Encoding: UTF8
-
-
-@InProceedings{Bodin2014Trusted,
- Title = {{A Trusted Mechanised {JavaScript} Specification}},
- Author = {Martin Bodin and Arthur Chargu{\'{e}}raud and Daniele Filaretti and Philippa Gardner and Sergio Maffeis and Daiva Naud\v{z}i\={u}nien\.{e} and Alan Schmitt and Gareth Smith},
- Booktitle = {Proceedings of the 41\textsuperscript{st} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2014},
- Pages = {87--100},
-
- Project = { web },
-
- Abstract = {JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
-We prconcurrencyesent JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.}
-}
-
-@Article{Calcagno2010Adjunct,
- Title = {{Adjunct elimination in Context Logic for Trees}},
- Author = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
- Journal = {Information and Computation},
- Year = {2010},
- Number = {5},
- Pages = {474--499},
- Volume = {208},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Calcagno2007Adjunct,
- Title = {{Adjunct Elimination in Context Logic for Trees}},
- Author = {Cristiano Calcagno and Thomas Dinsdale{-}Young and Philippa Gardner},
- Booktitle = {Proceedings of the 5\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
- Year = {2007},
- Pages = {255--270},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Calcagno2005From,
- Title = {{From Separation Logic to First-Order Logic}},
- Author = {Cristiano Calcagno and Philippa Gardner and Matthew Hague},
- Booktitle = {Proceedings of the 8\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
- Year = {2005},
- Pages = {395--409},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Calcagno2007Context,
- Title = {{Context Logic as Modal Logic: Completeness and Parametric Inexpressivity}},
- Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
- Booktitle = {Proceedings of the 34\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2007},
- Pages = {123--134},
-
- Project = { TBD },
-
- 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.}
-}
-
-@Article{Calcagno2007Local,
- Title = {{Local Reasoning about Data Update}},
- Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
- Journal = {Electronic Notes on Theoretical Computer Science},
- Year = {2007},
- Pages = {133--175},
- Volume = {172},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Calcagno2005Context,
- Title = {{Context Logic and Tree Update}},
- Author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
- Booktitle = {Proceedings of the 32\textsuperscript{nd} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2005},
- Pages = {271--282},
-
- Project = { TBD },
-
- 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.}
-}
-
-@Article{Cardelli2007Manipulating,
- Title = {{Manipulating Trees with Hidden Labels}},
- Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
- Journal = {Electronic Notes in Theoretical Computer Science},
- Year = {2007},
- Pages = {177--201},
- Volume = {172},
- doi = {10.1016/j.entcs.2007.02.007},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Cardelli2003Manipulating,
- Title = {{Manipulating Trees with Hidden Labels}},
- Author = {Luca Cardelli and Philippa Gardner and Giorgio Ghelli},
- Booktitle = {Proceedings of the 6\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
- Year = {2003},
- Pages = {216--232},
-
- Project = { TBD },
-
- 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.}
-}
-
-@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})},
- 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.}
-}
-
-@Article{Dawar2007Expressiveness,
- Title = {{Expressiveness and Complexity of Graph Logic}},
- Author = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
- Journal = {Information and Computation},
- Year = {2007},
- Number = {3},
- Pages = {263--310},
- Volume = {205},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Dawar2004Adjunct,
- Title = {{Adjunct Elimination Through Games in Static Ambient Logic}},
- Author = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli},
- Booktitle = {Proceedings of the 24\textsuperscript{th} International Conference on Foundations of Software Technology and Theoretical Computer Science ({FSTTCS})},
- Year = {2004},
- Pages = {211--223},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Dinsdale-Young2013Views,
- Title = {{Views: Compositional Reasoning for Concurrent Programs}},
- Author = {Thomas Dinsdale{-}Young and Lars Birkedal and Philippa Gardner and Matthew J. Parkinson and Hongseok Yang},
- Booktitle = {Proceedings of the 40\textsuperscript{th} Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2013},
- Pages = {287--300},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{Dinsdale-Young2010Concurrent,
- Title = {{Concurrent Abstract Predicates}},
- Author = {Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Matthew J. Parkinson and Viktor Vafeiadis},
- Booktitle = {Proceedings of the 24\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
- Year = {2010},
- Pages = {504--528},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{Dinsdale-Young2011Abstract,
- Title = {{Abstract Local Reasoning for Program Modules}},
- Author = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 4\textsuperscript{th} International Conference on Algebra and Coalgebra in Computer Science ({CALCO})},
- Year = {2011},
- Pages = {36--39},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Dinsdale-Young2010Abstraction,
- Title = {{Abstraction and Refinement for Local Reasoning}},
- Author = {Thomas Dinsdale{-}Young and Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 3\textsuperscript{rd} International Conference on Verified Software: Theories, Tools, Experiments ({VSTTE})},
- Year = {2010},
- Pages = {199--215},
-
- Project = { TBD },
-
- 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.}
-}
-
-@InProceedings{Gardner2010Reasoning,
- Title = {{Reasoning About Client-side Web Programs: Invited Talk}},
- Author = {Philippa Gardner},
- Booktitle = {Proceedings of the 2010 {EDBT/ICDT} Workshops, Lausanne, Switzerland, March 22-26, 2010},
- Year = {2010},
- doi = {10.1145/1754239.1754261},
-
- Project = { web },
-
- 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.}
-}
-
-@Article{Gardner2005Modelling,
- Title = {{Modelling Dynamic Web Data}},
- Author = {Philippa Gardner and Sergio Maffeis},
- Journal = {Theoretical Computer Science},
- Year = {2005},
- Number = {1},
- Pages = {104--131},
- Volume = {342},
-
- Project = { web },
-
- 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.}
-}
-
-@InProceedings{Gardner2003Modelling,
- Title = {{Modelling Dynamic Web Data}},
- Author = {Philippa Gardner and Sergio Maffeis},
- Booktitle = {Proceedings of 9\textsuperscript{th} International Workshop on Database Programming Languages ({DBPL})},
- Year = {2003},
- Pages = {130--146},
-
- Project = { web },
-
- 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.}
-}
-
-@InProceedings{Gardner2012Towards,
- Title = {{Towards a Program Logic for JavaScript}},
- Author = {Philippa Gardner and Sergio Maffeis and Gareth Smith},
- Booktitle = {Proceedings of the 39\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
- Year = {2012},
- Pages = {31--44},
-
- Project = { web },
-
- 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.}
-}
-
-@InProceedings{Gardner2014Local,
- Title = {{Local Reasoning for the {POSIX} File System}},
- Author = {Philippa Gardner and Gian Ntzik and Adam Wright},
- Booktitle = {Proceedings of the 23\textsuperscript{rd} European Symposium on Programming ({ESOP})},
- Year = {2014},
- Pages = {169--188},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@Article{Gardner2014Abstract,
- Title = {{Abstract Local Reasoning for Concurrent Libraries: Mind the Gap}},
- Author = {Philippa Gardner and Azalea Raad and Mark J. Wheelhouse and Adam Wright},
- Journal = {Proceedings of the 30\textsuperscript{th} Conference on the Mathematical Foundations of Programming Semantics ({MFPS})},
- Year = {2014},
- Pages = {147--166},
- Volume = {308},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{Gardner2015Trusted,
- Title = {{A Trusted Mechanised Specification of JavaScript: One Year On}},
- Author = {Philippa Gardner and Gareth Smith and Conrad Watt and Thomas Wood},
- Booktitle = {Proceedings of the 27\textsuperscript{th} International Conference on Computer Aided Verification ({CAV})},
- Year = {2015},
- Pages = {3--10},
-
- Project = { web },
-
- 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.}
-}
-
-@InProceedings{Gardner2008DOM,
- Title = {{DOM: Towards a Formal Specification}},
- Author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
- Booktitle = {Proceedings of the {ACM} {SIGPLAN} Workshop on Programming Language Technologies for XML ({PLAN-X})},
- Year = {2008},
-
- Project = { web },
-
- Abstract = {The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O'Hearn, Reynolds and Yang's local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g. invariant properties of simple Javascript programs.}
-}
-
-@InProceedings{Gardner2008Local,
- Title = {{Local Hoare Reasoning about {DOM}}},
- Author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
- Booktitle = {Proceedings of the 27\textsuperscript{th} {ACM} {SIGMOD-SIGACT-SIGART} Symposium on Principles of Database Systems ({PODS})},
- Year = {2008},
- Pages = {261--270},
-
- Project = { web },
-
- 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.}
-}
-
-@InProceedings{Gardner2009Small,
- Title = {{Small Specifications for Tree Update}},
- Author = {Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 6\textsuperscript{th} International Workshop on Web Services and Formal Methods ({WS-FM})},
- Year = {2009},
- Pages = {178--195},
-
- Project = { TBD },
-
- 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.}
-}
-
-@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)},
- 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,
- Title = {{Behavioural Equivalences for Dynamic Web Data}},
- Author = {Sergio Maffeis and Philippa Gardner},
- Journal = {Logic and Algebraic Programming},
- Year = {2008},
- Number = {1},
- Pages = {86--138},
- Volume = {75},
-
- Project = { web },
-
- 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. }
-}
-
-@InProceedings{Maffeis2004Behavioural,
- Title = {{Behavioural Equivalences for Dynamic Web Data}},
- Author = {Sergio Maffeis and Philippa Gardner},
- Booktitle = {Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {TCS}},
- Year = {2004},
- Pages = {535--548},
-
- Project = { web },
-
- 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.}
-}
-
-@InProceedings{Ntzik2015Reasoning,
- Title = {{Reasoning about the POSIX File System: Local Update and Global Pathnames}},
- Author = {Gian Ntzik and Philippa Gardner},
- Booktitle = {Proceedings of the 30\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
- Year = {2015},
- Month = {October},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{Ntzik2015Fault,
- Title = {{Fault-tolerant Resource Reasoning}},
- Author = {Gian Ntzik and Pedro {da Rocha Pinto} and Philippa Gardner},
- Booktitle = {Proceedings of the 13\textsuperscript{th} Asian Symposium on Programming Languages and Systems ({APLAS})},
- Year = {2015},
- Month = {December},
- Pages = {169--188},
- url = {http://dx.doi.org/10.1007/978-3-319-26529-2_10},
- doi = {10.1007/978-3-319-26529-2_10},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{Raad2015CoLoSL,
- Title = {{CoLoSL: Concurrent Local Subjective Logic}},
- Author = {Azalea Raad and Jules Villard and Philippa Gardner},
- Booktitle = {Proceedings of the 24\textsuperscript{th} European Symposium on Programming ({ESOP})},
- Year = {2015},
- Pages = {710--735},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{Raza2009Automatic,
- Title = {{Automatic Parallelization with Separation Logic}},
- Author = {Mohammad Raza and Cristiano Calcagno and Philippa Gardner},
- Booktitle = {Proceedings of the 18\textsuperscript{th} European Symposium on Programming ({ESOP})},
- Year = {2009},
- Pages = {348--362},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@Article{Raza2009Footprints,
- Title = {{Footprints in Local Reasoning}},
- Author = {Mohammad Raza and Philippa Gardner},
- Journal = {Logical Methods in Computer Science},
- Year = {2009},
- Number = {2},
- Volume = {5},
- doi = {10.2168/LMCS-5(2:4)2009},
- url = {https://arxiv.org/abs/0903.1032},
-
- Project = { concurrency },
-
- Abstract = {Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O'Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We formalise the notion of small specifications in local reasoning and show that for well-founded resource models, a smallest specification always exists that only includes the footprints, and also present results for the non-well-founded case. Finally, we investigate the conditions under which the footprints correspond to the smallest safe states, and present a heap model in which, unlike the standard model, this is the case for every program.}
-}
-
-@InProceedings{Raza2008Footprints,
- Title = {{Footprints in Local Reasoning}},
- Author = {Mohammad Raza and Philippa Gardner},
- Booktitle = {Proceedings of the 11\textsuperscript{th} International Conference on Foundations of Software Science and Computational Structures ({FOSSACS})},
- Year = {2008},
- Pages = {201--215},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{daRochaPinto2011Simple,
- Title = {{A Simple Abstraction for Complex Concurrent Indexes}},
- Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale{-}Young and Mike Dodds and Philippa Gardner and Mark J. Wheelhouse},
- Booktitle = {Proceedings of the 26\textsuperscript{th} Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA})},
- Year = {2011},
- Month = {October},
- Pages = {845--864},
- url = {http://doi.acm.org/10.1145/2048066.2048131},
- doi = {10.1145/2048066.2048131},
-
- Project = { concurrency },
-
- 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.}
-}
-
-@InProceedings{daRochaPinto2014TaDA,
- Title = {{TaDA: A Logic for Time and Data Abstraction}},
- Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale{-}Young and Philippa Gardner},
- Booktitle = {Proceedings of the 28\textsuperscript{th} European Conference on Object-Oriented Programming ({ECOOP})},
- Year = {2014},
- Month = {July},
- Pages = {207--231},
- url = {http://dx.doi.org/10.1007/978-3-662-44202-9_9},
- doi = {10.1007/978-3-662-44202-9_9},
-
- Project = { concurrency, tada },
-
- 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.}
-}
-
-@InProceedings{daRochaPinto2015Steps,
- Title = {{Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)}},
- Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner},
- Booktitle = {Proceedings of the 31\textsuperscript{st} Conference on the Mathematical Foundations of Programming Semantics ({MFPS})},
- Year = {2015},
- Month = {June},
- Pages = {3--18},
- url = {http://www.sciencedirect.com/science/article/pii/S1571066115000699},
- doi = {10.1016/j.entcs.2015.12.002},
-
- Project = { concurrency },
-
- Abstract = {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.}
-}
-
-@InProceedings{daRochaPinto2016Modular,
- Title = {Modular Termination Verification for Non-blocking Concurrency},
- Author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner and Julian Sutherland},
- Booktitle = {Proceedings of the 25\textsuperscript{th} European Symposium on Programming ({ESOP})},
- Year = {2016},
- Month = {April},
- Pages = {176--201},
- url = {http://dx.doi.org/10.1007/978-3-662-49498-1_8},
- doi = {10.1007/978-3-662-49498-1_8},
-
- 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.},
-
- Project = { concurrency, tada }
-}
-
-@inproceedings{Raad2016Verifying,
- Title = {Verifying Concurrent Graph Algorithms},
- Author = {Azalea Raad and Aquinas Hobor and Jules Villard and Philippa Gardner},
- Booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
- Year = {2016},
- Pages = {314--334},
- url = {http://dx.doi.org/10.1007/978-3-319-47958-3_17},
- doi = {10.1007/978-3-319-47958-3_17},
- Project = { concurrency },
-
- 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.}
-}
-
-@inproceedings{Raad2016DOM,
- Title = {{DOM:} Specification and Client Reasoning},
- Author = {Azalea Raad and Jos{\'{e}} {Fragoso Santos} and Philippa Gardner},
- Booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
- Year = {2016},
- Pages = {401--422},
- url = {http://dx.doi.org/10.1007/978-3-319-47958-3_21},
- doi = {10.1007/978-3-319-47958-3_21},
- Project = { web },
-
- 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.}
-}
-
-@InProceedings{Dinsdale-Young2017Caper,
- Title = {Caper: Automatic Verification for Fine-grained Concurrency},
- Author = {Thomas Dinsdale-Young and Pedro {da Rocha Pinto} and Kristoffer Just Andersen and Lars Birkedal},
- Booktitle = {Proceedings of the 26\textsuperscript{th} European Symposium on Programming ({ESOP})},
- Year = {2017},
- Month = {April},
-
- 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.},
-
- Project = { concurrency }
-}
-
-@InProceedings{Xiong2017Abstract,
- Title = {Abstract Specifications for Concurrent Maps},
- Author = {Shale Xiong and Pedro {da Rocha Pinto} and Gian Ntzik and Philippa Gardner},
- Booktitle = {Proceedings of the 26\textsuperscript{th} European Symposium on Programming ({ESOP})},
- Year = {2017},
- Month = {April},
-
- 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.},
-
- Project = { concurrency, tada }
-}
-@Article{Fragoso2016Mashic,
- Title = {{Mashic Compiler: Mashup Sandboxing based on Inter-frame Communication}},
- Author = {Zhengqin Luo and Jos{\'{e}} {Fragoso Santos} and Ana Almeida Matos and Tamara Rezk},
- Journal = {Journal of Computer Security},
- Year = {2016},
- Number = {24},
- Volume = {1},
- Pages = {91--136},
- doi = {10.3233/JCS-160542},
- url = { http://dx.doi.org/10.3233/JCS-160542},
-
- 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.},
-
- Project = { web }
- }