_posts/2017-05-03-consistency.md

+---
+title: Philippa Gardner, talk at the open Workshop on Consistency in Distributed Storage Systems, LIP6, Paris
+---
+Philippa Gardner gave a talk on "A Concurrent Specification of PoSIX" at the open workshop "[Consistency in distributed storage](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/)".
+organised by [Marc Shapiro](https://pages.lip6.fr/Marc.Shapiro/) [(UPMC-LIP6 and  Inria)](https://www.inria.fr/).
+
+This year's workshop, held at the Université Pierre et Marie Curie - LIP6, Paris, France on 3 May 2017, offered students 
+and academics an opportunity to share insights on the principles and practice of distributed data replication systems, 
+based on solid distributed algorithm and engineering principles. The workshop is held under the aegis of the French ANR Project RainbowFS, 
+which aims to deconstruct consistency and to develop principled tools for the design, verification, deployment and monitoring, 
+and to use them for developing a correct-by-construction and efficient geo-scale petabyte-sized storage system.
+
+Philippa’s abstract and slides are available on the [workshop page](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/).

_posts/2017-05-08-aarhus.md

+---
+title: Visit to Aarhus University and Aarhus Concurrency Workshop
+---
+
+Philippa Gardner, Azalea Raad, Andrea Cerone and Emanuele D'Osualdo will be attending the [Aarhus Concurrency Workshop on Concurrency Theory](http://conferences.au.dk/acw/) and related topics at the end of month.
+
+This year's workshop is organised by [Thomas Dinsdale-Young](http://cs.au.dk/~tyoung/), who was previously a PhD and PostDoc with Philippa.
+Andrea Cerone will give a talk on [Algebraic Laws for Weak Consistency](http://conferences.au.dk/acw/abstracts/). 
+The workshop will take place at the Department of Computer Science 
+at [Aarhus University](http://cs.au.dk/research/) on May 30 and 31 and 
+is the latest in a series previously held at [University of Kent](https://www.cs.kent.ac.uk/events/kcw/), 
+[Imperial College London](http://multicore.doc.ic.ac.uk/icw2015/), [The University of York](https://www-users.cs.york.ac.uk/~miked/ycw2014/), 
+[University of Oxford](http://www.cs.ox.ac.uk/people/hongseok.yang/ccw12/index.html), [Trinity College Dublin](https://www.scss.tcd.ie/Vasileios.Koutavas/dcw2011/),
+[Cambridge University](https://www-users.cs.york.ac.uk/~miked//ccw2010/index.html), Newcastle, 
+and [Queen Mary](https://web.archive.org/web/20100606005049/http://www.eecs.qmul.ac.uk/~ohearn/Workshops/Concurrency09/).
+
+Aarhus is the second largest city in Denmark and is one of the 2017 [European Capitals of Culture](http://www.aarhus2017.dk/en/).

_posts/2017-05-09-Kloos.md

+---
+title: Johannes Kloos, visitor from MPI
+---
+[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.
+
+The talk abstract: I will present work on a program logic and associated type system for reasoning about asynchronous programs manipulating shared 
+mutable state. The logic and type system guarantee the absence of races and the preservation of user-specified invariants using a combination of two ideas: 
+refinement types and concurrent separation logic. The logic track ownership of shared state across concurrently posted tasks and allow reasoning about 
+ownership transfer between tasks using permissions. The type system integrated the logic with refinement types to reason about the contents of the heap, 
+in presence of asynchronous tasks. I will first demonstrate the type system on examples from OCaml, and afterwards sketch some preliminary 
+work in applying it to JavaScript.
\ No newline at end of file

_posts/2017-05-17-Gian.md

+---
+title: Goodbye to Dr Gian Ntzik, moving to Amadeus
+---
+Best wishes to Dr Gian Ntzik, who will move to [Amadeus](http://www.amadeus.com/web/amadeus/en_GB-GB/Amadeus-Home/About-us/Our-company/1319477448520-Page-AMAD_DetailPpal)
+at the end of May to work in systems development and research.
+
+Amadeus is one of the top ten providers of sofware in the world, especialising in sofware for the travel and tourism industry.  
+Amadeus employs over 14,000 people worldwide and is currently the largest provider of global distribution (GDS) systems in the world.
\ No newline at end of file

_posts/2017-05-25-Azalea.md

+---
+title: Congratulations to Azalea Raad, joining the Max Planck Institute for Software Systems, Germany
+---
+
+Many congratulations to Dr Azalea Raad, who has accepted a position as a Postdoctoral Fellow at the 
+[Max Planck Institute for Software Systems](https://www.mpi-sws.org/) in Kaiserslautern, Germany, starting in July.
+
+Azalea will work with [Viktor Vafeiadis](https://people.mpi-sws.org/~viktor/) and [Derek Dreyer](https://people.mpi-sws.org/~dreyer/) 
+on weak memory models for transactions, a new exciting area with much left to explore. Azalea's thesis and recent publications are now available 
+on [her website](http://www.soundandcomplete.org/publications.html).
\ No newline at end of file

_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