_posts/2017-05-25-ecma.md

+---
+title: Philippa Gardner, invited talk at the Ecma TC39 meeting, Google, NY
+---
+Philippa Gardner was invited to give a talk about JavaScript Verification at the
+[TC39 – ECMAScript Task group standards committee meeting](http://www.ecma-international.org/memento/TC39-RF-TG.htm) held at Google, New York, this May. 
+
+Philippa gave a talk entitled: "Towards Trustworthy Verification of JavaScript" at the Visions for the future of ECMAScript / Emerging technologies session of the meeting.
+The TC39 Task Group oversees the standardization of the general purpose, cross platform, vendor-neutral ECMAScript (JavaScript) programming language. 
+This includes the language syntax, semantics, and libraries and complementary technologies that support the language.
\ No newline at end of file

_posts/2017-06-13-csf.md

+---
+title: Paper accepted at CSF'17 
+---
+Emanuele D'Osualdo has had a paper accepted at this year's [Computer Security Foundations Symposium (CSF)](http://csf2017.tecnico.ulisboa.pt/index.html).
+
+Emanuele's paper, in collaboration with [Luke Ong](http://www.cs.ox.ac.uk/luke.ong/), University of Oxford, UK and [Alwen Tiu](http://www.ntu.edu.sg/home/atiu/), 
+Nanyang Technological University, Singapore, is entitled ['Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes'](http://www.emanueledosualdo.com/research/papers/2017/csf-decidable-secrecy.html).
+
+In the paper, the authors 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 placed on the class is a notion of depth-boundedness. 
+They 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 real-world symmetric key protocols, including Needham-Schroeder Symmetric Key, 
+Otway-Rees, and Yahalom.
+
+CSF'17 is an annual conference for researchers in computer security, to examine current theories of security, 
+the formal models that provide a context for those theories, and techniques for verifying security. 
+Originally a workshop of the [IEEE Computer Society's Technical Committee on Security and Privacy](http://www.ieee-security.org/), 
+the meeting became a “symposium” in 2007, with a number of important papers and techniques having been presented first at CSF. 
+This year's papers are now available on the [CSF'17 conference's website](http://csf2017.tecnico.ulisboa.pt/accepted.html).

_posts/2017-06-16-Algebraic.md

+---
+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]({{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.
+CONCUR is part of [QONFEST](https://conference.imp.fu-berlin.de/qonfest/home), the umbrella event comprising the joint international 2017 meetings [CONCUR](https://www.concur2017.tu-berlin.de),
+[QEST](http://www.qest.org/qest2017), [FORMATS](http://formats17.ulb.be), and [EPEW](http://page.mi.fu-berlin.de/preineck/epew2017-mirror), alongside with several workshops and tutorials.
\ No newline at end of file

_posts/2017-07-03-urops.md

+---
+title: Welcome to UROP students 
+---
+We are delighted to welcome Thomas Pointon, Samuel Ogunmola and Ashley Davies-Lyons 
+who will be working with the group this summer as part of Imperial’s 
+[Undergraduate Research Opportunities Programme (UROP)](http://www.imperial.ac.uk/urop).
\ No newline at end of file

_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 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) 
+
+ 
+The demo illustrated how JaVerT can be used to specify and verify a JavaScript priority queue implementation, 
+showcasing the abstractions provided by JaVerT for reasoning about the JavaScript semantics, with an emphasis on objects, 
+prototype chains, and function closures, as well as the infrastructure for supporting arbitrary user-defined recursive predicates. 
+ 
+JaVerT is a semi-automatic verification tool chain for JavaScript based on separation logic. It targets functionally correct specifications 
+of critical JavaScript software, in particular small Node.js libraries that have high usability: for example, those describing well-known data structures, 
+such as a priority queue. JaVerT provides a wide variety of built-in abstractions so that our specifications are straightforward, 
+despite the underlying complexity of the JavaScript semantics.
+ 
+JSTools’s aim is to bring together participants from academia and industry working on the analysis of JavaScript and its dialects, 
+to share ideas and problems, with a focus on presentations of shareable infrastructure.
\ No newline at end of file

_posts/2017-08-12-cade.md

+---
+title: Invited paper at the 26th International Conference on Automated Reasoning, (CADE), Gothenburg, Sweden.
+---
+
+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]({{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. 
+It also highlights the difficulties imposed by the language and the current state-of-the-art in the literature.
+
+The conference on Automated Deduction (CADE) is the major international forum at which research on all aspects 
+of automated deduction is presented. The conference, first established in 1974, is held under the aegis of the [Association for Automated Reasoning (AAR)](http://www.aarinc.org)
\ No newline at end of file

_posts/2017-09-06-darmstadt.md

+---
+title:  Philippa Gardner, Keynote talk at Reliably Secure Software Systems (RS3) meeting, Darmstadt, Germany.
+---
+Philippa Gardner gave a keynote talk entitled 'Trustworthy Software Specification' at the [final event](http://www.spp-rs3.de/final-event/) 
+of the [DFG-funded]( http://www.dfg.de/en/dfg_profile/mission/index.html) national research initiative ["Reliably Secure Software Systems (RS3)"](http://www.spp-rs3.de).
+
+![Participants at RS3 Darmstadt 2017](/images/posts/Darmstadt-participants.jpg)
+
+The meeting, which took place on 4-6 September 2017 in Darmstadt, Germany, featured presentations of selected results from RS3 research 
+and invited [keynotes]( http://www.spp-rs3.de/final-event/keynotes.html) by renowned international speakers.
+The overall goal of [RS3]( http://www.spp-rs3.de/About) has been to enable a reliable verification of system-wide 
+security guarantees based on a well-founded understanding of programs and of security aspects.
\ No newline at end of file

_posts/2017-09-22-fmats5.md

+---
+title: Fifth Workshop on Formal Methods and Tools for Security (FMATS5)
+---
+
+Almost a hundred participants attended this year’s FMATS, held on 21-22 September 2017 at Microsoft Research Cambridge. 
+
+The workshop, now on its fifth year, was attended by researchers, PhD students, industrialists and government employees 
+with a common interest in formal methods and verification. The programme included 19 specialist talks, poster presentations 
+and a session of short talks for PhD students, RAs and industrialists to introduce themselves to each other and the audience. 
+For a list of the talks and slides [please see this year’s programme](https://vetss.org.uk/fmats-timetable/).
+
+![FMATS5 Welcome session](/images/posts/Welcome-to-FMATS5-768x488.png)
+
+You can also see [photos of the two days on the FMATS5 Flickr page](https://www.flickr.com/gp/143382439@N02/42SQU9).
\ No newline at end of file

_posts/2017-09-26-popl.md

+---
+title: Paper accepted at POPL 2018
+---
+[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/).
+
+The paper is entitled JaVerT: JavaScript Verification using Separation Logic and introduces 
+[JaVerT](http://ec2-52-56-105-125.eu-west-2.compute.amazonaws.com:3000/javert ) 
+a semi-automatic verification tool chain for JavaScript based on separation logic. More details will follow soon! 
\ No newline at end of file

_posts/2017-10-02-gabriela.md

+---
+
+title: Welcome to Gabriela Sampaio, new PhD student with the group
+
+---
+
+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), 
+a refactoring tool for Erlang, under the supervision of [Prof Simon Thompson](https://www.cs.kent.ac.uk/people/staff/sjt/). After a stint as a  web developer in Brazil,
+she went back to UFPE in 2017 to do a MSc under the supervision of [Prof Paulo Borba](http://ufpe.academia.edu/PauloBorba), working on ways to support developers in partially 
+safe changes to software product lines with the use of a partial refinement theory; the results were published at [SPLC'16](https://dl.acm.org/citation.cfm?id=2934482). 
+Gabriela's PhD thesis will focus on the reasoning and verification of large Javascript Programs.
\ No newline at end of file

_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