_posts/2017-02-06-ESOP.md

@@ -3,17 +3,17 @@ title: Papers accepted at ESOP 2017
 ---
 
 Two papers from the concurrency project team have been accepted at 26th European Symposium on Programming [(ESOP 2017)](http://www.etaps.org/index.php/2017/esop),
-which will take place this April in Uppsala, Sweden. The first paper, [Abstract Specifications for Concurrent Maps](https://psvg.doc.ic.ac.uk/publications/Xiong2017Abstract.html), present the importance of abstract atomicity for reasoning fine-grained concurrent modules.
-The second paper, [Caper: Automatic Verification for Fine-grained Concurrency](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html), presents a prototype tool for automated reasoning about concurrent modules. 
+which will take place this April in Uppsala, Sweden. The first paper, [Abstract Specifications for Concurrent Maps]({{site.baseurl}}{% link publications/Xiong2017Abstract.html %}), present the importance of abstract atomicity for reasoning fine-grained concurrent modules.
+The second paper, [Caper: Automatic Verification for Fine-grained Concurrency]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}), presents a prototype tool for automated reasoning about concurrent modules. 
 
-The first paper, submitted by [Shale Xiong](https://psvg.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto](https://psvg.doc.ic.ac.uk/people/da-rocha-pinto.html), 
-[Gian Ntzik](https://psvg.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner](https://psvg.doc.ic.ac.uk/people/gardner.html),
-[Abstract Specifications for Concurrent Maps](https://psvg.doc.ic.ac.uk/publications/Xiong2017Abstract.html) demonstrates that abstract atomicity 
+The first paper, submitted by [Shale Xiong](https://vtss.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}), 
+[Gian Ntzik](https://vtss.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}),
+[Abstract Specifications for Concurrent Maps]({{site.baseurl}}{% link publications/Xiong2017Abstract.html %}) demonstrates that abstract atomicity 
 is key to give a specification for concurrent map that allows better client reasoning.
 This paper also provides the first functional correctness proof of ConcurrentSkiplistMap in java.util.concurrent with respect to the abstract specification.
 
 The second paper accepted, submitted by Pedro Da Rocha Pinto, in collaboration with [Thomas Dinsdale-Young](http://cs.au.dk/~tyoung/), 
 [Kristoffer Just Andersen](http://pure.au.dk/portal/en/persons/id(5e842a19-8b76-487a-8082-06b6d6ff2545).html)
-and [Lars Birkedal](http://www.cs.au.dk/~birke/) from Aarhus University is [Caper: Automatic Verification for Fine-grained Concurrency](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html).
+and [Lars Birkedal](http://www.cs.au.dk/~birke/) from Aarhus University is [Caper: Automatic Verification for Fine-grained Concurrency]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}).
 The paper presents [Caper](https://github.com/caper-tool/caper), a prototype tool for automated reasoning about concurrent modules.
 Caper is based on symbolic execution, integrating reasoning about interference on shared resources. This enables Caper to verify the functional correctness of fine-grained concurrent modules.

_posts/2017-05-09-Kloss.md → _posts/2017-05-09-Kloos.md

 ---
-title: Johannes Kloss, visitor from MPI
+title: Johannes Kloos, visitor from MPI
 ---
-[Johannes Kloss]( https://people.mpi-sws.org/~jkloos/), a fourth-year PhD student at the [Max Planck Institute for Software Systems](https://www.mpi-sws.org/) 
+[Johannes Kloos]( https://people.mpi-sws.org/~jkloos/), a fourth-year PhD student at the [Max Planck Institute for Software Systems](https://www.mpi-sws.org/) 
 visited the group this week. 
 
 Johannes gave a talk to the group about his current research, on Reasoning about event-based concurrency with Asynchronous Liquid Separation Types.

_posts/2017-06-16-Algebraic.md

@@ -4,7 +4,7 @@ title: Paper accepted at Concur 2017
 Andrea Cerone has had a paper accepted at this year’s [International Conference on Concurrency Theory, (Concur 2017)](https://www.concur2017.tu-berlin.de/) 
 which will be held in Berlin, Germany in September.
 
-The paper, entitled [Algebraic Laws for Weak Consistency](https://psvg.doc.ic.ac.uk/publications/Cerone2017Algebraic.html) was written in collaboration 
+The paper, entitled [Algebraic Laws for Weak Consistency]({{site.baseurl}}{% link publications/Cerone2017Algebraic.html %}) was written in collaboration 
 with [Alexey Gotsman]( http://software.imdea.org/~gotsman), IMDEA Software Institute, Madrid and [Hongseok Yang](http://www.cs.ox.ac.uk/people/hongseok.yang/Public/Home.html), University of Oxford, UK.
 
 The purpose of the CONCUR conferences is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications. The topics covered are Theory, Formal Modelling, Verification, Performance Evaluation and Engineering of concurrent, timed, and other systems.

_posts/2017-07-07-jstools.md

 ---
 title: Demo on the use of JaVerT at the JSTools'17 workshop
 ---
-José Fragoso Santos gave a talk and demo on the use of [JaVerT](http://j3fsantos.github.io) at the [JSTools'17 workshop](http://2017.ecoop.org/track/JSTools-2017-papers#program), 
+José Fragoso Santos gave a talk and demo on the use of JaVerT at the [JSTools'17 workshop](http://2017.ecoop.org/track/JSTools-2017-papers#program), 
 part of this year’s European Conference on Object-Oriented Programming [(ECOOP 2017).](http://2017.ecoop.org) 
 
  

_posts/2017-08-12-cade.md

@@ -5,7 +5,7 @@ title: Invited paper at the 26th International Conference on Automated Reasoning
 Philippa Gardner was one of the invited speakers at the this year’s [CADE conference](http://www.cade-26.info/), held in Gothenburg, Sweden, on 6-11 August 2017. 
 
 Philippa presented an invited paper, [‘Towards Logic-based Verification of JavaScript Programs’](https://link.springer.com/chapter/10.1007/978-3-319-63046-5_2), 
-jointly written with [José Fragoso Santos](https://psvg.doc.ic.ac.uk/people/fragoso-santos.html), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/) 
+jointly written with [José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/) 
 and [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/) 
 
 This position paper proposes a possible pathway to achieve scalable symbolic verification of JavaScript based on separation logic. 

_posts/2017-09-26-popl.md

 ---
 title: Paper accepted at POPL 2018
 ---
-[José Fragoso Santos](https://psvg.doc.ic.ac.uk/people/fragoso-santos.html), [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), 
+[José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}), [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), 
 [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/) 
 and [Thomas Wood](https://www.doc.ic.ac.uk/~tw1509/), have had a paper accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages 
 [(POPL 2018)](https://popl18.sigplan.org/).

_posts/2017-10-02-gabriela.md

@@ -4,7 +4,7 @@ title: Welcome to Gabriela Sampaio, new PhD student with the group
 
 ---
 
-We are really happy to welcome [Gabriela Sampaio](https://psvg.doc.ic.ac.uk/people/sampaio.html), who has joined the group as a PhD student. 
+We are really happy to welcome [Gabriela Sampaio]({{site.baseurl}}{% link _people/sampaio.md %}), who has joined the group as a PhD student. 
 
 Gabriela completed her BSc at the Federal University of Pernambuco (UFPE, Brazil)
 and as an undergraduate, she spent a year at the University of Kent, working on [Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html), 

_posts/2017-11-15- bernardi.md

+---
+title: Visitor to the group, Giovanni Bernardi, IRIF, Paris
+---
+
+[Dr Giovanni Bernardi](https://www.researchgate.net/profile/Giovanni_Bernardi2) of Paris Diderot University / [IRIF]( https://www.irif.fr//en/index) 
+visited the group in November to give a talk on his current work on must- testing for message passing concurrency. 
+
+[Giovanni](https://www.irif.fr/~gio/index.xhtml) is a long standing co-author with Andrea Cerone and has worked on Formal methods 
+and the Semantics of programming languages, focusing on concurrency, types (overall behavioural ones [BETTY]), and models of types. 
+The title of his talk was Full-abstraction for Must Testing Preorders. 
+
+Abstract: The client must preorder relates tests (clients) instead of processes (servers). 
+The existing characterisation of this preorder is unsatisfactory for it relies 
+on the notion of usable clients which, in turn, are defined using an existential 
+quantification over the servers that ensure client satisfaction. In this talk, 
+we characterise the set of usable clients for finite-branching LTSs, and give a 
+sound and complete decision procedure for it. We also provide a novel coinductive 
+characterisation of the client preorder, which we use to argue that the preorder 
+is decidable, thus positively answering the question remained open in the literature.

_posts/2017-11-24-siddharth.md

+---
+title: Visitor to the group, Siddharth Krishna, New York University, USA
+---
+We are very pleased to have welcomed [Siddharth Krishna](https://cs.nyu.edu/~siddharth/), from the [Courant Institute of Mathematical Sciences, NYU](https://cims.nyu.edu/), 
+who visited the group this week to talk about his work on the verification of concurrent data structures.
+
+Siddharth is a PhD student in the Computer Science Department of New York University, working on Formal Verification and Machine Learning under the supervision 
+of [Thomas Wies](https://cs.nyu.edu/wies/). Siddharth gave a talk based on his forthcoming paper on Flow Interfaces: [Go with the Flow: Compositional Abstractions 
+for Concurrent Data Structures](https://cs.nyu.edu/~siddharth/pubs/2018-popl-flows.pdf), joint work with Dennis Shasha and Thomas Wies, to appear 
+at [POPL 2018](https://popl18.sigplan.org/home).
+
+The abstract of the talk is: 
+
+Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. 
+However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting, such as inductive predicates, 
+are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting 
+regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated 
+with the node that is computed as a fixpoint over the entire heap graph. We refer to this quantity as a flow. Flows can encode both structural properties 
+of the heap (e.g. the reachable nodes from the root form a tree) as well as data invariants (e.g. sortedness). We then introduce the notion of a flow interface, 
+which expresses the relies and guarantees that a heap region imposes on its context to maintain the local flow invariant with respect to the global heap. 
+Our main technical result is that this notion leads to a new semantic model of separation logic. In this model, flow interfaces provide a general abstraction 
+mechanism for describing complex data structures. This abstraction mechanism admits proof rules that generalize over a wide variety of data structures. 
+To demonstrate the versatility of our approach, we show how to extend the logic RGSep with flow interfaces. We have used this new logic to prove linearizability 
+and memory safety of nontrivial concurrent data structures. In particular, we obtain parametric linearizability proofs for concurrent dictionary algorithms 
+that abstract from the details of the underlying data structure representation. These proofs cannot be easily expressed using the abstraction mechanisms 
+provided by existing separation logics.
\ No newline at end of file

_posts/2017-12-07-google-summit-munich.md

+---
+title: Google Compiler and Programming Language Summit, Munich, Germany
+---
+
+[Gabriela Sampaio](https://www.doc.ic.ac.uk/~gcs817/) and [Shale Xiong](https://www.doc.ic.ac.uk/~sx14/) were two of the invited students attending 
+this year’s Google Compiler and Programming Language Summit in Munich, Germany.
+ 
+
+The summit, now on its fifth year, invites a number of promising PhD students 
+across Europe working in the field of compiler and programming language technology, 
+to attend three days of research talks and seminars at the Google office. 
+ 
+Gabriela and Shale took part in the poster fair, presenting two posters about their current work on 
+[Automatic JavaScript Program Verification Using Bi-Abduction]({{site.baseurl}}{% link slides/Sampaio-Automatic-JavaScript.pdf %})
+and [Reasoning about Concurrent Programs using Separation Logic]({{site.baseurl}}{% link slides/Xiong-Concurrent.pdf %}).
+
+They also attended several round tables and had the chance to discuss their 
+research with engineers at Google and to learn first hand
+about Google’s latest work on programming language implementation and how this 
+research is applied to compilers and language tooling at Google and across industry.
\ No newline at end of file

_posts/2018-01-06-PhD_opportunity.md

+---
+title: PhD position, start date in October 2018
+---
+
+Philippa Gardner is currently looking for a PhD student, start date in October 2018, 
+to join the [Verified Trustworthy Software Specification Group]({{site.baseurl}}), 
+ 
+
+For more details, please see the note below from Philippa:
+
+I am looking for a PhD student to start in October 2018 to join my research group on program analysis and specification, 
+as part of the [analysis and verification theme at Imperial](http://www.imperial.ac.uk/computing/research/analysis-and-verification/).
+My group is involved with a a wide range of theoretical and practical projects on the analysis and verification of concurrent and web programs. Possible projects include:
+* a theoretical project on reasoning about either concurrent algorithms (see [MFPS'15 tutorial paper](https://www.doc.ic.ac.uk/~pg/publications/daRochaPinto2015Steps.pdf))
+or distributed systems (a new topic for me since [Andrea Cerone](https://www.doc.ic.ac.uk/~acerone/) became my RA; 
+* a more practical project on using our concurrent specification of POSIX file systems for verification and testing 
+(see Ntzik's [PhD thesis](https://www.doc.ic.ac.uk/~pg/publications/Ntzik2017Reasoning.pdf));
+* several projects associated with the JaVert verification toolchain (see [POPL'18 paper](https://www.doc.ic.ac.uk/~jfaustin/javert.pdf)); and 
+* several projects associated with test generation from language semantics (see [POPL’14 paper](https://www.doc.ic.ac.uk/~pg/publications/Bodin2014Trusted.pdf))
+or library axiomatic specifications.
+
+A successful UK student will probably be funded through the standard Departmental competition for funds. A successful 
+EU/overseas student will probably be funded by a combination of Departmental funding and my funding. 
+
+The deadlines to apply for a PhD position in the Department are **19 January 2018** and 23 March 2018. 
+The Department advises all students requiring funding to apply by the January deadline, 
+although there may still be some funding available for applications received after January. 
+Further details can be found at the in the Department's [PhD application page](http://www.imperial.ac.uk/computing/prospective-students/phd/). 
+
+Please do not hesitate to [contact me directly](https://www.doc.ic.ac.uk/~pg/#contact) if interested, 
+
+Best wishes, Philippa
\ No newline at end of file

_posts/2018-01-12-popl.md

+---
+title: Paper presented at POPL18
+---
+
+[José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}) presented his paper 
+[JaVerT: JavaScript Verification using Separation Logic]({{site.baseurl}}{% link publications/FragosoSantos2018JaVerT.html %}), jointly authored 
+with [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/),
+[Thomas Wood](https://www.doc.ic.ac.uk/~tw1509/) and [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), at this year’s ACM SIGPLAN Symposium on Principles 
+of Programming Languages [(POPL 2018)](https://popl18.sigplan.org/).
+
+The paper introduces JaVerT, a semi-automatic verification tool chain for JavaScript 
+based on separation logic.
+
+<div style="position:relative;height:0;padding-bottom:56.25%"><iframe src="https://www.youtube.com/embed/HDf5PC0bzzo?ecver=2" style="position:absolute;width:100%;height:100%;left:0" width="640" height="360" frameborder="0" allow="autoplay; encrypted-media" allowfullscreen></iframe></div>
+
+
+
+More videos recorded during the conference are available on the [POPL18 YouTube channel](https://www.youtube.com/channel/UCTp2XBEhj5rBzc2IfysZwYA). 
\ No newline at end of file

_posts/2018-01-15-tech_talk.md

+---
+title: Tech talk at Galois, Philippa Gardner
+---
+
+Philippa Gardner was invited to give a tech talk at [Galois, Portland, USA]( https://galois.com/) on Javert, a JavaScript Verification Toolchain. 
+
+JaVerT is a semi-automatic JavaScript Verification Toolchain based on separation 
+logic aimed at the specialist developer wanting rich, mechanically verified specifications 
+of critical JavaScript code. We address three main challenges: the specification 
+challenge is to design specifications that are readable by developers; 
+the verification challenge is to handle the complex, dynamic nature of 
+JavaScript without simplification; finally the validation challenge 
+is to understand what it means for the verification to be trusted.
+
+You can see a video of the talk [on the Galois Youtube channel](https://youtu.be/uNVAmCYL1Jo).  
\ No newline at end of file

_posts/2018-01-29-grohens.md

+---
+title: Welcome to Theotime Grohens, internship working on JaVert.
+---
+
+We are very happy to welcome [Theotime Grohens](https://angel.co/theotime-grohens) who will be spending three months with the group at the beginning of the year. 
+
+Theotime is currently a Master student at the École normale supérieure school in Paris, working with  Pierre Senellart. While at the group, Theo will work on extending JaVerT, the JavaScript Verification Toolchain.   
\ No newline at end of file

_posts/2018-01-31-chungkilhur.md

+---
+title: Visitor to the group, Dr Chung-Kil Hur, Seoul National University.
+---
+
+[Dr Chung-Kil Hur](http://sf.snu.ac.kr/gil-hur/) of the Seoul National University came to visit the group and to talk about 
+a [promising semantics for relaxed-memory concurrency](http://sf.snu.ac.kr/promise-concurrency/), [published at POPL'17](http://sf.snu.ac.kr/promising/release/promising.pdf) 
+and joint work with Jeehoon Kang from Seoul National University, and Ori Lahav, Viktor Vafeiadis and Derek Dreyer from MPI-SWS.
+
+The talk abstract:
+
+The "promising semantics" is an operational semantics for relaxed-memory concurrency that can account for concurrency features of major programming languages such 
+as C/C++ and Java.  The semantics is promising since (1) it adequately balances the conflicting desiderata of programmers, compilers, and hardware, which has been 
+a long standing open problem; (2) it is (arguably) simple and easy to understand because it is a standard interleaving operational semantics with just two new notions: 
+"view" and "promise"; and (3) most results are fully formalized in Coq. In this talk, I will introduce (1) the basics of relaxed memory concurrency, 
+(2) the challenges with defining its model, and (3) the promising semantics showing how it solves the challenges.
\ No newline at end of file

_posts/2018-02-14-hu-talk.md

+---
+title: Talk by Dr Justin Hsu, From Couplings to Probabilistic Relational Program Logics
+---
+
+[Dr Justin Hsu](https://popl18.sigplan.org/profile/justinhsu) of University College of London visited the group this week to give a talk about probabilistic 
+coupling: "From Couplings to Probabilistic Relational Program Logics".
+
+Justin Hsu, a graduate from the University of Pennsylvania is currently a post-doctoral researcher at the University College of London. 
+His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory. 
+
+The talk abstract was:
+
+Many program properties are relational, comparing the behavior of a program (or even two different programs) on two different inputs. 
+While researchers have developed various techniques for verifying such properties for standard, deterministic programs, relational properties 
+for probabilistic programs have been more challenging. In this talk, I will survey recent developments targeting a range of probabilistic relational 
+properties, with motivations from privacy, cryptography, machine learning. The key idea is to meld relational program logics with an idea from probability theory, 
+called a probabilistic coupling. The logics allow a highly compositional and surprisingly general style of analysis, supporting clean proofs for a variety of 
+probabilistic relational properties.
\ No newline at end of file

_posts/2018-03-01-daiva-thesis.md

+---
+title: Congratulations to Dr Daiva Naudžiūnienė
+---
+
+Many congratulations to [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/), 
+who very successfully defended her PhD thesis, [An Infrastructure for Tractable 
+Verification of JavaScript Programs]( https://vtss.doc.ic.ac.uk/publications/Naudziuniene2018Infrastructure.html) 
+on Monday 1st March.
+
+Also many thanks to [Matthew Parkinson](https://www.microsoft.com/en-us/research/people/mattpark/), 
+[Tamara Rezk](https://www-sop.inria.fr/lemme/Tamara.Rezk/) and [Susan Eisenbach](http://www.imperial.ac.uk/people/s.eisenbach) 
+who acted as the examiners.
\ No newline at end of file

_posts/2018-03-19-formal-methods-meets-js.md

+---
+title: Formal Methods Meets JavaScript Workshop
+redirect_from: /2018/03/14/formal-methods-meets-js.html
+---
+On Monday 19th March, we hosted a day of research talks on Programming Languages Formal Methods
+researchers on topics including language specification, program verification, etc. with a focus on
+research relating to the JavaScript language and ecosystem.
+
+This event was organised to coincide with the March 2018 TC39 ECMAScript standards committee meeting at
+Imperial and thus allow TC39 members and researchers working in the field to meet during an informal workshop.
+
+You can find a list of the speakers and the slides for their talks below
+
+  * [Avik Chaudhuri](https://avikchaudhuri.github.io/), Facebook California -- [Safe Types in Untyped Contexts]({{site.baseurl}}{% link slides/Safe_types_untyped_contexts.pdf %}) 
+  * [Anders Møller](https://cs.au.dk/~amoeller/), Aarhus University -- [Systematic Approaches for Increasing Soundness and Precision of Static Analyzers]({{site.baseurl}}{% link slides/Systematic_approaches_for_increasing_soundness_and_precision_of_static_analyzers.pdf %})
+  * [Karthik Bhargavan](http://prosecco.gforge.inria.fr/personal/karthik/), Inria Paris -- [Verifying Cryptographic Web Applications]({{site.baseurl}}{% link slides/Verifying_Cryptographic_Web_Application.pdf %})
+  * [Nadim Kobeissi](https://nadim.computer/), Inria Paris & Symbolic Software -- [Bringing Formal Verification to the Real Web: Three Years of Interconnected Work]({{site.baseurl}}{% link slides/Towards_Formal_Verification_in_Cryptographic_Web_Applications.pdf %})
+  * [Andreas Rossberg](https://people.mpi-sws.org/~rossberg/), Dfinity -- [Neither Web nor Assembly]({{site.baseurl}}{% link slides/Neither_Web nor_Assembly.pdf %})
+  * [Conrad Watt](https://www.cl.cam.ac.uk/~caw77/), Cambridge University -- [Adventures in Mechanising and Verifying WebAssembly]({{site.baseurl}}{% link slides/adventures_in_machanising_and_verifying_webassembly.pdf %})
+  * [Mark S. Miller](https://research.google.com/pubs/author35958.html), Google -- [Verify what? Navigating the Attack Surface]({{site.baseurl}}{% link slides/Verify_what_Navigating_the_Attack_Surface.pdf %})
+  * [Erik Krogh Kristensen](https://webbies.dk/), Aarhus University -- [Testing and Evolving TypeScript Declaration Files with Program Analysis]({{site.baseurl}}{% link slides/Testing_and_Evolving_TypeScript_Declaration_Files_with_Program_Analysis.pdf %})
+  * [Sophia Drossopoulou](https://wp.doc.ic.ac.uk/sd/), Imperial College London -- [Reasoning for Open Systems]({{site.baseurl}}{% link slides/Reasoning_for_Open_Systems.pdf %})
+  * [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/), Imperial College London -- [Logic-based Verification of JavaScript Programs]({{site.baseurl}}{% link slides/ECMA_JaVerT.pdf %})
+  * [Johannes Kinder](http://www.cs.rhul.ac.uk/home/kinder/), Royal Holloway, University of London -- [Practical Dynamic Symbolic Execution of Standalone JavaScript]({{site.baseurl}}{% link slides/Practical_Dynamic_Symbolic_Execution_of_Standalone_JavaScript.pdf %})
+  * [Alan Schmitt](http://people.rennes.inria.fr/Alan.Schmitt/), Inria Rennes -- [From JSCert to JSExplain and Beyond]({{site.baseurl}}{% link slides/From_JSCert_to_JSExplain_and_beyond.pdf %})

_posts/2018-04-18-papers-accepted-april-18.md

+---
+title: Paper accepted and paper published
+---
+
+A paper co-authored by current and former researchers of the group has just been 
+publised. A second paper, also collaborative work with current and former researchers 
+has also just been accepted to ECOOP 18.
+
+The first paper, [A perspective on specifying and verifying concurrent modules](https://www.sciencedirect.com/science/article/pii/S2352220817300871)
+by [Thomas Dinsdale-Young](https://cs.au.dk/~tyoung/), [Pedro da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}) 
+and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}) has been published in the [Journal of Logical and Algebraic Methods in Programming](https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming).
+
+In the paper, the authors survey a range of techniques for specifying concurrent modules, 
+using the example of a counter module to illustrate the benefits and limitations of each.
+They highlight four key concepts underpinning these techniques: auxiliary state, 
+interference abstraction, resource ownership and atomicity. Then they demonstrate how 
+these concepts can be combined to achieve two powerful approaches for specifying 
+concurrent modules and verifying implementations and clients, which remove the 
+limitations highlighted by the counter example.
+
+The second paper, co-authored by [Gian Ntzik]({{site.baseurl}}{% link _people/ntzik.md %}), 
+[Pedro da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}), 
+[Julian Sutherland]({{site.baseurl}}{% link _people/sutherland.md %})
+and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}) has just been accepted to the 32nd European Conference on Object-Oriented Programming 
+[(ECOOP 2018)](https://conf.researchr.org/home/ecoop-2018), which will be held in Amsterdam in July. 
+
+In the paper, entitled A Concurrent Specification of POSIX File Systems, 
+the authors provide a formal concurrent specification of POSIX file systems 
+and demonstrate scalable reasoning for clients.
+
+Congratulations to all.
\ No newline at end of file

_posts/2018-04-23- felix-stutz.md

+---
+title: Welcome to Felix Stutz
+---
+
+We are very pleased to welcome Felix Stutz, an MSc student at 
+the [International Max Planck Research School for Computer Science](http://www.imprs-cs.de/index.html), 
+who is due to spend five months with the group, working with Emanuele D'Osualdo 
+on Ideal completions for Verification of Cryptographic Protocols. 
+
+These protocols are distributed programs that are designed to achieve secure 
+communications using cryptography; they are notoriously very tricky to design 
+and reasoning about the security properties of these protocols requires proving 
+that no malicious intruder can hack the protocol to gain sensitive information, 
+e.g. your emails.
+
+In fact, every time you log in to your email account, make an online payment or 
+connect to a secure Wi-Fi (and in many other scenarios!) the communication is 
+made secure under the hood by the use of such cryptographic protocols. 
+The project's goal is to develop new algorithms to verify that a protocol does not leak any secret.
+
+For the theoretical basis for the project please 
+see [this paper](http://www.emanueledosualdo.com/research/papers/2017/csf-decidable-secrecy.html) 
+by D'Osualdo and others, which proposes a new approach for model checking cryptographic protocols.
\ No newline at end of file