_posts/2018-06-13-martin.md

+---
+title: Welcome to Martin Bodin, new member of the group
+---
+We are very happy to welcome Martin Bodin, who joins the group as a Research Associate. 
+Martin did his PhD on [Certified Semantics and Analysis of JavaScript](http://www.cmm.uchile.cl/~mbodin/doktorigxo/manuscrit.pdf)
+at the [University of Rennes 1](https://english.univ-rennes1.fr/) under the supervision 
+of [Alan Schmitt]( http://people.rennes.inria.fr/Alan.Schmitt/index.html) 
+and [Thomas Jensen](http://www.irisa.fr/celtique/jensen/). He then 
+participated on the [JSCert project]( http://www.jscert.org/) to build 
+a Coq specification for JavaScript. 
+
+He applied the same formalising technique to build a semantics for R during his 
+postdoc at the [University of Chile]( http://www.cmm.uchile.cl/). These specifications 
+come with a high degree of confidence, but also with a large size. His current 
+work focuses on building and proving abstract analyses for such large semantics.
+
+You can find more about Martin and his work on [his webpage](http://www.cmm.uchile.cl/~mbodin/esplorado.html?lang=en#en).
\ No newline at end of file

_posts/2018-07-16-seminar.md

+---
+title: Seminar by Felix Stutz on Automated Verification of Security Protocols 
+---
+Felix Stutz gave a talk on Monday on Automated Verification of Security Protocols. He 
+presented the latest work on the project he is doing with Emanuele D’Osualdo and which will inform his Master Thesis.
+
+The abstract is: 
+Security protocols are distributed programs that are designed to achieve secure 
+communications using cryptography. A distinctive feature of the security properties 
+of protocols is that they must hold in the presence of an active adversarial 
+environment, and this makes them challenging to verify. An important example 
+of such a security property is secrecy: can the protocol leak a (secret) message 
+to the environment as a result of interference by the intruder?
+This project's goal is to develop a new algorithm to verify secrecy of cryptographic 
+protocols with unbounded sessions and nonces.
+The novelty of the approach, based on a new decidability result 
+by [D'Osualdo et al. (CSF17)](http://vtss.doc.ic.ac.uk/publications/DOsualdo2017Deciding.html), 
+is in how the unboundedness caused by the use of unlimited nonces can be tamed 
+algorithmically. We will present a new verification algorithm for secrecy based 
+on symbolic representations of inductive invariants of protocols. 
\ No newline at end of file

_posts/2018-09-01-marie_curie.md

+---
+title: Congratulations to Emanuele D’Osualdo, Marie-Curie Fellowship
+---
+
+Many congratulations to Emanuele, whose project “Verification through Security 
+and Progress Abstractions” (VeSPA) was awarded a two year [Marie-Curie Individual 
+Fellowship](https://ec.europa.eu/research/mariecurieactions/actions/individual-fellowships_en), 
+hosted at Imperial College. 
+
+Emanuele will be working with Philippa Gardner to explore 
+new ways to effectively prove Progress (aka liveness) and Security (eg. secrecy) 
+of concurrent programs. You can find more details of the project 
+[on his blog](https://www.emanueledosualdo.com/blog/2018/announce-marie-curie-fellowship.html).
\ No newline at end of file

_posts/2018-09-02-fellowship.md

+---
+title: Philippa Gardner, Established Career Fellowship, VeTSpec, Verified Trustworthy Software Specification
+---
+Philippa Gardner has been awarded an Established Career Fellowship by the UK Research and Innovation (UKRI). 
+
+Under the title [“VeTSpec: Verified Trustworthy Software Specification”](https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/R034567/1), 
+the five-year fellowship will support Philippa work in exploring the fundamental, 
+conceptual questions associated with bringing the scientific, mathematical method 
+to the specification of modern software systems.
\ No newline at end of file

_posts/2018-09-03-radu.md

+---
+title: IBM Project Prize to Radu Szasz, Msc project supervised by Philippa Gardner and Jose Fragoso
+---
+
+Congratulations to [Radu Szasz](https://github.com/raduszasz) (MEng Computing Year 4), 
+who was awarded the IBM Project Prize for his MsC project, [Typing JavaScript via 
+Symbolic Execution](https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1718-ug-projects/Radu-Szasz-Typing-JavaScript-via-Symbolic-Execution.pdf), supervised by Philippa Gardner and Jose Fragoso. 
+
+The IBM Project Prize recognizes outstanding achievement in an individual undergraduate 
+project the Department of Computing. Over the summer, Radu worked with Philippa Gardner and Jose 
+Fragoso to build a mechanism for using TypeScript type annotations 
+as light-weight specifications for JaVerT, a static analysis tool based on Separation 
+Logic. He then applied that approach to a number of examples, and was 
+able to achieve a 40-fold reduction in the specification character count. Radu 
+is due to join Facebook London as a Software Engineer in October. Congratulations 
+and good luck!
\ No newline at end of file

_posts/2018-10-15-sacha.md

+---
+title: Welcome to Sacha Ayoun, new PhD student with the group
+---
+
+We are very happy to welcome [Sacha Ayoun](https://www.doc.ic.ac.uk/~sja3417/), who has joined the group as a PhD student. 
+
+Sacha will work on JavaScript Verification using separation logic, under the supervision 
+of Philippa Gardner. Sacha completed his Supelec Engineer Diploma at [CentraleSupelec](http://www.centralesupelec.fr/) 
+in 2018 as well as his MSc in Advanced Computing at Imperial. During his undergraduate 
+course he was a researcher-engineer intern at the [French Alternative and Atomic Energy Commission (CEA)](http://www.cea.fr/english),
+where he worked improving the Frame-C abstract interpreter to better handle file descriptors.
\ No newline at end of file

_posts/2018-11-10-popl19.md

+---
+title: Papers accepted at POPL 2019
+---
+
+Congratulations to José Fragoso Santos, Philippa Gardner, Petar Maksimović, 
+Martin Bodin and Gaby Sampaio, whose papers were accepted at this year’s 
+[ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019)](https://popl19.sigplan.org/home).
+
+José, Petar, Gaby and Philippa had their paper ['JaVerT 2.0: Compositional 
+Symbolic Execution for JavaScript']({{site.baseurl}}{% link publications/FragosoSantos2019JaVerT.html %}) accepted. The paper describes JaVerT 2.0, 
+a symbolic analysis tool for JavaScript that follows the language semantics 
+without simplifications. 
+
+Martin and Philippa's paper, written in collaboration with 
+[Thomas Jensen](http://www.irisa.fr/celtique/jensen/) and 
+[Alan Schmitt](http://people.rennes.inria.fr/Alan.Schmitt/), 
+from [Inria]( https://www.inria.fr/en/centre/rennes), is ['Skeletal Semantics 
+and Their Interpretations']({{site.baseurl}}{% link publications/Bodin2019Skeletal.html %}) and in it, they introduce a skeletal semantics of 
+a language, where each skeleton describes the complete semantic behaviour of 
+a language construct. You can find more details and additional proofs on the [companion page](http://skeletons.inria.fr/popl2019/index.html)
+and their [artifact on their Gitlab repository](https://gitlab.inria.fr/skeletons/Coq/tree/POPL2019).
\ No newline at end of file

_posts/2018-11-7-facebook.md

+---
+title: Facebook Continuous Reasoning research award for JaVerT 2.0.
+---
+
+Philippa Gardner, Jose Fragoso Santos and Petar Maksimovic have won a [Facebook 
+Continuous Reasoning research award](https://research.fb.com/announcing-the-winners-of-the-facebook-continuous-reasoning-research-awards/) 
+for their project JaVerT 2.0: Automatic Compositional Analysis for JavaScript.  
+
+[JaVerT 2.0](https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2019JaVerT.pdf) 
+is a separation-logic-based tool for JavaScript analysis and testing that follows 
+the language semantics without simplifications. It supports whole-program symbolic 
+testing, verification, and automatic compositional testing based on bi-abduction.
+The award, one of five awarded on the call, was open to research teams working on 
+[applying formal methods using continuous reasoning and in particular, those addressing 
+fundamental problems for mostly-automatic or interactive verifiers.](https://research.fb.com/programs/research-awards/proposals/continuous-reasoning-research-award/)
\ No newline at end of file

_posts/2019-04-01-eccop2019.md

+---
+title: Paper accepted at ECOOP 2019
+---
+
+Congratulations to Petar Maksimović and Philippa Gardner, whose paper with 
+[Conrad Watt](https://www.cl.cam.ac.uk/~caw77/) and [Neel Krishnaswami](https://www.cl.cam.ac.uk/~nk480/)
+(University of Cambridge) has been accepted at this year’s [European Conference 
+on Object-Oriented Programming (ECOOP '19)](https://2019.ecoop.org/)
+
+In their paper: [“A Program Logic for First-Order Encapsulated WebAssembly”](https://2019.ecoop.org/event/ecoop-2019-papers-a-program-logic-for-first-order-encapsulated-webassembly) 
+they introduce Wasm Logic, a sound program logic for first-order, encapsulated 
+WebAssembly. Using Wasm Logic, they also specify and verify a simple WebAssembly 
+tree library, giving abstract specifications independent of the underlying implementation. 
+You can [read the draft submitted for publication here](https://www.cl.cam.ac.uk/~nk480/wasm-pl.pdf).
\ No newline at end of file

_posts/2019-05-1- fMfSS_talk.md

+---
+title: Talk at Formal Methods for Statistical Software workshop, Martin Bodin
+---
+[Martin Bodin](https://vtss.doc.ic.ac.uk/people/bodin.html) gave a talk “A Trustworthy Mechanized Formalization of R“ at the 
+[Formal Methods for Statistical Software (FMfSS 2019)](https://samate.nist.gov/FMSwVRodeo/FMfSS2019.html) 
+workshop, to present his work on big-step operational semantics for R.  The abstract for the talk is below. 
+
+The FMfSS workshop aims to identify formal methods, tools, and techniques that 
+can be used to gain higher assurance of statistical software. The workshop is 
+co-located with the [High Confidence Software and Systems Conference](https://cps-vo.org/group/hcss_conference) 
+and is organised by the U.S. Census Bureau and the [National Institute of Standards and Technology (NIST)]( https://www.nist.gov/)
+
+Abstract: The R programming language is very popular for developing statistical 
+software and data analysis, thanks to rich libraries, concise and expressive syntax, 
+and support for interactive programming. Yet, the semantics of R is fairly complex, 
+contains many subtle corner cases, and is not formally specified. This makes 
+it difficult to reason about R programs.
+In this work, we develop a big-step operational semantics for R in the form of 
+an interpreter written in the Coq proof assistant. We ensure the trustworthiness 
+of the formalization by introducing a monadic encoding that allows the Coq interpreter, 
+CoqR, to be in direct visual correspondence with the reference R interpreter, 
+GNU R. Additionally, we provide a testing framework that supports systematic 
+comparison of CoqR and GNU R. In its current state, CoqR covers the nucleus 
+of the R language as well as numerous additional features, making it pass 
+a significant number of realistic test cases from the GNU R and FastR projects. 
+To exercise the formal specification, we prove in Coq the preservation 
+of memory invariants in selected parts of the interpreter. 
+This work is an important first step towards a robust environment for 
+formal verification of R programs.
\ No newline at end of file

_posts/2019-05-13-lorentz _seminar.md

+---
+title: Effective Verification Workshop at the Lorentz centre, talks by Philippa Gardner and Emanuele D’Osualdo
+---
+
+Philippa Gardner and Emanuele D'Osualdo gave invited talks as this May's Lorentz centre workshop: 
+[Effective Verification: Static Analysis Meets Program Logics]( http://lorentzcenter.nl/lc/web/2019/1115/description.php3?wsid=1115&venue=Snellius) in Leiden, The Netherlands.
+
+Philippa gave a talk on TADA Live: Compositional Reasoning for the Termination 
+of Fine-grained Concurrent Programs and Emanuele gave a talk entitled: Inductive 
+Invariants for Automatic Verification of Cryptographic Protocols.
+
+The [Lorentz Center workshop series](http://lorentzcenter.nl/progsel.php) 
+brings together scientists in a work environment that fosters exchange and 
+interaction and the establishment of collaborations. For the [Effective 
+Verification workshop](http://lorentzcenter.nl/lc/web/2019/1115/description.php3?wsid=1115&venue=Snellius), 
+the centre invited researchers in both static analysis and program logics 
+(e.g. concurrent separation logic) and encouraged them to share each other's 
+techniques and tools. The goal is to help promote work developing more effective 
+automation for program logics (using techniques from static analysis), as well 
+as help extend static analysis to prove more daring properties beyond safety 
+(using techniques from program logics).
+ 
+You can find the [programme of the workshop here](http://lorentzcenter.nl/lc/web/2019/1115/program.pdf)
+
+![Effective Verification Static Analysis Meets Program Logics poster](/images/posts/Lorentz.jpg)
\ No newline at end of file

_posts/2019-05-31-goodbye _andrea.md

+---
+title: Goodbye to Dr Andrea Cerone
+---
+
+Our very best wishes to Andrea Cerone, who after three years with the group is 
+leaving to take up a position as a software engineer for [Footballradar](https://www.footballradar.com/).
\ No newline at end of file

_posts/2019-06-03-calco.md

+---
+title: 8th Conference on Algebra and Coalgebra in Computer Science
+---
+Philippa Gardner and Emanuele D’Osualdo are part of the local organising team for 
+[the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)](https://www.coalg.org/calco-mfps-2019/calco/) 
+which is taking place in London this week. 
+
+CALCO aims to bring together researchers and practitioners with interests in 
+foundational aspects, and both traditional and emerging uses of algebra and coalgebra 
+in computer science. It takes place alongside the [35th Conference on the 
+Mathematical Foundations of Programming Semantics (MFPS 2019)](https://www.coalg.org/calco-mfps-2019/mfps/)
+
+[The conference programme](https://www.coalg.org/calco-mfps-2019/programme/) and [list 
+of accepted papers](https://www.coalg.org/calco-mfps-2019/calco/calco19-list-of-accepted-papers/) are now available from the [conference website](https://www.coalg.org/calco-mfps-2019/calco/). 

_posts/2019-07-26-srepls.md

+---
+title: Emanuele D'Osualdo and Shale Xiong, talks at Surrey Concurrency Workshop and S-REPLS
+---
+
+Emanuele D'Osualdo and Shale Xiong both gave talks at this year's [Surrey Concurrency Workshop 
+and S-REPLS](https://cw-srepls-19.github.io/#schedule).
+
+The two-day workshop, which was hosted by the [University of Surrey this year](https://cw-srepls-19.github.io/#previous), is aimed at 
+bringing together researchers working on the theory of concurrency and the 
+semantics and implementation of programming languages. 
+
+You can find the abstract for Emanuele’s talk on [TaDA Live](https://cw-srepls-19.github.io/abstracts.html#gardner)
+and Shale’s talk on [Data Consistency in Transactional Storage Systems](https://cw-srepls-19.github.io/abstracts.html#xiong) 
+on the [workshop page](https://cw-srepls-19.github.io/abstracts.html#gardner).
\ No newline at end of file

_posts/2019-08-09-marktoberdorf.md

+---
+title: Summer School Marktoberdorf 2019
+---  
+Gaby Sampaio and Sacha Ayoun, two of the group’s PhD students, were invited to 
+attend the [40th Marktoberdorf Summer School](https://www2.in.tum.de/mod19/index.html), 
+organised by the [Technical University of Munich (TUM)](https://www.tum.de/). 
+
+The Summer School Marktoberdorf is a 10-day course for young computer scientists 
+and mathematicians working on formal approaches to correctness and security of software systems. 
+This year’s topic was “Safety and Security for Software Systems: Logics, Proofs, 
+Applications” and the focus was on the latest verification tools developed to 
+mechanize the design of safe and secure programs. The busy programme, with lectures, 
+keynotes and presentations had a particular emphasis on Logics and Logical-based 
+Methods and mathematical reasoning about safety and security and protection against 
+failure, and also included sports days, socials and a visit to Neuschwanstein Castle.
+
+![One of the presentations during the summer school](/images/images/Marktoberdorf.jpg)
\ No newline at end of file

_posts/2019-08-15-jose.md

+---
+title: Goodbye to Jose Fragoso
+---
+
+Goodbye and good luck to Jose Fragoso, who is moving to the 
+[Instituto Superior Técnico, Lisbon, Portugal](https://tecnico.ulisboa.pt/pt/) 
+to become an Assistant Professor in the [Department of Computer Science and 
+Engineering](https://fenix.tecnico.ulisboa.pt/departamentos/dei/o-dei). 
+
+Jose will be conducting his research as part of the [SAT group](https://inesc-id.pt/group/II08/) 
+at the [INESC-ID]( https://inesc-id.pt/about-us/#).
\ No newline at end of file

_posts/2019-09-26-workshop.md

+---
+title: Workshop on Verified Software, Isaac Newton Institute for Mathematical Sciences, Cambridge.
+---
+Philippa Gardner was one of the organisers of the [`Verified Software’ 
+workshop](https://vetss.org.uk/vetss-verified-software-workshop-24th-25th-september-2019/), 
+held at the [Isaac Newton Institute for Mathematical Sciences, (INI)](http://www.newton.ac.uk/), 
+Cambridge on 24th-25th September 2019.
+
+The workshop was organised by [VeTSS, the Research Institute in Verified Trustworthy 
+Software Systems](https://vetss.org.uk/) working in partnership with the Newton 
+Gateway to Mathematics and the Isaac Newton Institute (INI). The two day workshop 
+is a forerunner to [the INI’s six-week summer programme on `Verified Software’ 
+in the summer of 2020](http://www.newton.ac.uk/event/vso).
+The programme of the two days, together with slides and videos of the talks can 
+be downloaded from the [workshop page](https://vetss.org.uk/verified-software-workshop-programme/).
+
+![Future Challenges Discussion with Tony Hoare, John Goodacre and Philippa Gardner](/images/posts/Verified-Software-Workshop.jpg)
\ No newline at end of file

_posts/2019-10-01-internship.md

+---
+title: Internship at Facebook, Infer Team
+---
+
+Julian Sutherland has just returned from a three months internship with the Facebook's Infer team. 
+
+While at Facebook, Julian worked to develop a static analysis tool for [Infer]( https://fbinfer.com/), 
+quandryBO, intended to statically find unchecked array accesses tainted by user-provided 
+information. He also worked on extending the capabilities of the current infer 
+buffer overflow analysis, InferBO and dealing with function calls within infer's 
+intermediate representation, SIL. 
+
+[Infer is a static analysis tool]( https://github.com/facebook/infer) for Java, 
+C++, Objective-C, and C which was [open-sourced in 2015]( https://engineering.fb.com/developer-tools/open-sourcing-facebook-infer-identify-bugs-before-you-ship/).
\ No newline at end of file

_posts/2019-10-28-iris.md

+---
+title: Talk at Iris Workshop, Aarhus University, Denmark
+---
+Philippa Gardner, Emanuele D’Osualdo and Julian Sutherland attended the first edition 
+of the [Iris workshop](https://iris-project.org/workshop-2019/#program).
+
+The two-day workshop, held at Aarhus University, Denmark focused on [Iris]( https://iris-project.org/), 
+a Higher-Order Concurrent Separation Logic Framework implemented and verified 
+in the proof assistant Coq that can be used for reasoning about safety of concurrent programs.
+
+Philippa gave a talk on their joint work on “Compositional Reasoning for the Termination of Fine-grained Concurrent Programs”.
\ No newline at end of file

_posts/2019-10-30-livestream.md

+---
+title: Facebook testing and verification symposium, 20-21 November, livestream
+---
+The [third annual Facebook testing and verification symposium](https://fbtavsymposium2019.splashthat.com/?gz=0949d2b64c045dc1ebb599012c988f37&pp=1&guest-access-hash=NDU3NDYzOTg2fDI2MzM0NTExOHwxNTcyMzg4MzY1OzYyMDc1MTc5MDZiODM5YjNiMzExNDA0ZTllNzUyNjhhZDlmNzk4OTk3N2RmMzZlMjY4Y2VmY2ZjYTE0YmI3MTI=) 
+will be held on 20-21 November in London. 
+
+This is a two-day programme of talks which aims to increase the collaboration 
+and exchange between testing and verification scientific research in academia 
+and industry.
+
+Many of the talks will be available to watch on livestream, for details see 
+the [event page](https://fbtavsymposium2019.splashthat.com/?gz=0949d2b64c045dc1ebb599012c988f37&pp=1&guest-access-hash=NDU3NDYzOTg2fDI2MzM0NTExOHwxNTcyMzg4MzY1OzYyMDc1MTc5MDZiODM5YjNiMzExNDA0ZTllNzUyNjhhZDlmNzk4OTk3N2RmMzZlMjY4Y2VmY2ZjYTE0YmI3MTI=).
\ No newline at end of file