.gitlab-ci.yml

@@ -3,7 +3,7 @@ stages:
   - build
   - deploy
 
-image: "ruby:2.6-stretch"
+image: "ruby:2.6-buster"
 variables:
   NOKOGIRI_USE_SYSTEM_LIBRARIES: "true"
 
@@ -20,6 +20,7 @@ build:
     - triggers
   tags:
     - docker
+    - vtss_site
   before_script:
     - bundle install --deployment --without=development --with=test
     - bundle exec rake init
@@ -36,6 +37,7 @@ deadlinks:
     - triggers
   tags:
     - docker
+    - vtss_site
   before_script:
     - bundle install --deployment --without=development --with=test
   script:
@@ -47,6 +49,7 @@ deploy:
   image: resourcereasoning/website-deploy
   tags:
     - docker
+    - vtss_site
   only:
     - master
   except:
@@ -71,6 +74,7 @@ update_publications:
   image: ignoredambience/github-gitlab-sync
   tags:
     - docker
+    - vtss_site
   only:
     - triggers
   before_script:

.gitmodules

 [submodule "publications"]
 	path = publications
-	url = https://gitlab.doc.ic.ac.uk/resource-reasoning/publications.git
+	url = https://gitlab.doc.ic.ac.uk/verified-software/publications.git
 	branch = master

Dockerfile

+FROM ruby:2.6
+
+# throw errors if Gemfile has been modified since Gemfile.lock
+RUN bundle config --global frozen 1
+RUN gem install bundler:1.16.6
+
+WORKDIR /usr/src/app
+
+COPY Gemfile Gemfile.lock ./
+RUN bundle install
+
+COPY . .
+
+RUN bundle exec rake init
+
+EXPOSE 4000
+
+CMD ["bundle", "exec", "jekyll", "serve", "--host", "0.0.0.0"]
\ No newline at end of file

_people/ayoun.md

@@ -15,9 +15,8 @@ the supervision of Professor Philippa Gardner. He is currently working
 on [Gillian](https://gillianplatform.github.io), a parametric symbolic execution 
 tool for symbolic testing, verification and automatic compositional testing.
 
-During his undergraduate 2017, Sacha worked at the [French Alternative and Atomic Energy Commission
-(CEA)](http://www.cea.fr/english) as a researcher-engineer intern.
-His goal was to improve the Frame-C abstract interpreter to better handle
-file descriptors. In 2018 he completed his Supelec Engineer Diploma
-at [CentraleSupelec](http://www.centralesupelec.fr/)
-as well as his MSc in Advanced Computing at Imperial.
\ No newline at end of file
+As an undergraduate, Sacha worked at the [French Alternative and Atomic Energy Commission
+(CEA)](http://www.cea.fr/english) as a researcher-engineer intern in 2017. His goal was 
+to improve the Frame-C abstract interpreter to better handle file descriptors. 
+In 2018 he completed his Supelec Engineer Diploma at [CentraleSupelec](http://www.centralesupelec.fr/)
+as well as his MSc in Advanced Computing at Imperial.

_people/gardner.md

@@ -28,8 +28,8 @@ Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to
 Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS.
 She obtained a lectureship at Imperial in 2001, and became professor in 2009.
 She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior
-Fellowship at Imperial, 2005-2009.
+Fellowship at Imperial, 2005-2009. 
 
 Philippa directs the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/),
 funded by EPSRC and NCSC, 2017-2022. She is an organiser
-of the [Isaac Newton Institute six-week summer programme on `Verified Software', 2020](http://www.newton.ac.uk/event/vso).
\ No newline at end of file
+of the [Isaac Newton Institute six-week summer programme on `Verified Software', 2022](https://www.newton.ac.uk/event/vso2/). In 2020 she was elected a [Fellow of the Royal Academy of Engineering](https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2020/fellows/professor-philippa-gardner).

_people/karmios.md

+---
+firstname: Nat
+lastname: Karmios
+position: Researcher
+webpage: 
+email: nathaniel.karmios18@imperial.ac.uk
+github: 
+alumnus: false
+projects:
+---
+
+Nat Karmios is a Research Engineer in Imperial's Verified Software Group under Professor Philippa Gardner, working on [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), a parametric symbolic execution tool for symbolic testing, verification and automatic compositional testing.
+
+After earning their MEng in Computing at Imperial - completing their thesis project with the group - Nat has brought their years of industry engineering experience to improve Gillian's accessibility through the development of a visual debugger for symbolic execution and verification.

_people/loow.md

+---
+firstname: Andreas
+lastname: Lööw
+position: Researcher
+webpage: https://www.doc.ic.ac.uk/~aloow/
+email: a.loow@imperial.ac.uk
+github: https://github.com/AndreasLoow
+alumnus: false
+projects:
+---
+
+Andreas did his PhD at Chalmers University of Technology, in Sweden, under the supervision of [Magnus Myreen](http://www.cse.chalmers.se/~myreen/). At Chalmers, Andreas worked on interactive theorem proving for software and hardware correctness. Specifically, he worked on building trustworthy computer systems, known as verified stacks, with full-system correctness theorems. Much of his work revolved around trustworthy hardware, for example in the form of the development and verification of the [Verilog synthesis tool Lutsig](https://dl.acm.org/doi/10.1145/3437992.3439916). Andreas defended his thesis, [Building Verified Hardware and Verified Stacks in HOL](https://www.doc.ic.ac.uk/~aloow/papers/thesis.pdf), in September 2021.

_people/maksimovic.md

@@ -6,7 +6,7 @@ position: Researcher
 webpage: https://sites.google.com/site/petarmaksimovic1981/
 email: p.maksimovic@imperial.ac.uk
 github: PetarMax
-alumnus: false
+alumnus: true
 projects:
   - web
   - moc
@@ -14,6 +14,6 @@ projects:
   - gillian
 ---
 
-Petar Maksimović is a Research Fellow with the group and the Academic Program Manager for the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/).
+Petar Maksimović was a Research Fellow with the group and the Academic Program Manager for the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/) until his move to industry in 2022.
 
-He also holds the position of Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.
\ No newline at end of file
+Petar is also a Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.

_people/nantes.md

+---
+firstname: Daniele
+lastname: Nantes
+position: Researcher
+webpage: 
+email: d.nantes-sobrinho@imperial.ac.uk
+github:  
+alumnus: false
+projects:
+---
+
+[Daniele](https://mat.unb.br/dnantes/) is a tenured assistant professor at the Department of Mathematics, University of Brasília, and is currently in a long sabbatical leave. 
+
+Daniele's research focusses on equational reasoning and comparative expressiveness of models and languages with concurrency.  She was a researcher with the [Theoretical Computer Science Group (GTC-UnB)](https://www.mat.unb.br/ayala/TCgroup/index.html), and an external collaborator of the [VIDI project Unifying Correctness for Communicating Systems](https://www.jperez.nl/vidi). Her latest publications are [Formalising nominal C-unification generalised with protected variables](https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/formalising-nominal-cunification-generalised-with-protected-variables/0299ECF29C28FDD65AAE38E73BF28FE3), published in Mathematical Structures for Computer Science, and the conference papers [Nominal Equational Problems](https://link.springer.com/chapter/10.1007/978-3-030-71995-1_2), published in ETAPS’ Foundations of Software Science and Computation Structures (FOSSACS 2021) series, and [Non-deterministic Functions as Non-Deterministic Processes](https://drops.dagstuhl.de/opus/volltexte/2021/14259/), in Formal Structures for Computation and Deduction (FSCD 2021) series.

_people/naudziuniene.md

@@ -6,6 +6,6 @@ position: PhD Student
 alumnus: true
 ---
 
-Daiva defended her Ph.D. on [An Infrastructure for Tractable Verification of JavaScript Programs]({{site.baseurl}}{% link publications/Naudziuniene2018Infrastructure.html %}) in March 2018.
+Daiva defended her PhD on [An Infrastructure for Tractable Verification of JavaScript Programs]({{site.baseurl}}{% link publications/Naudziuniene2018Infrastructure.html %}) in March 2018.
 
-Since 2017, Daiva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.
\ No newline at end of file
+Since 2017, Daiva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.

_people/sampaio.md

@@ -3,18 +3,13 @@ firstname: Gabriela
 lastname: Sampaio
 position: PhD Student
 webpage: https://www.doc.ic.ac.uk/~gcs817/
-email: g.sampaio17@imperial.ac.uk
+email:
 github:  
-alumnus: false
+alumnus: true
 projects:
   - web
   - moc
 ---
-Gabriela Sampaio is a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
+Gabriela Sampaio was a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
 Imperial, under the supervision of Professor Philippa Gardner. 
-She completed her BSc course at Federal University of Pernambuco (UFPE, Brazil) in 2015. 
-During the undergraduate course, she spent one year at the University of Kent, working on an Erlang refactoring project ([Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html)) 
-under the supervision of Professor Simon Thompson. Later in 2017, she completed her MSc, also at UFPE, under supervision of Professor Paulo Borba. 
-The work aims 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). Between the MSc and the PhD, Gabriela worked as a web developer in Brazil. 
-Her PhD thesis will focus on the reasoning and verification of large Javascript Programs.
+She completed her BSc  and MSc at Federal University of Pernambuco (UFPE, Brazil), spending a year abroad at the University of Kent, working on the Erlang refactoring project ([Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html)). In 2022, Gabriela defended her PhD thesis, [A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS](https://spiral.imperial.ac.uk/bitstream/10044/1/100397/1/CunhaSampaio-G-2022-PhD-Thesis.pdf), and took up a position at Meta (formerly Facebook).

_people/sutherland.md

@@ -3,12 +3,11 @@ firstname: Julian
 lastname: Sutherland
 position: PhD Student
 webpage: http://www.doc.ic.ac.uk/~jhs110/
-email: jhs110@doc.ic.ac.uk
-alumnus: false
+email: 
+alumnus: true
 projects:
   - concurrency
   - sl
 ---
 
-Julian is a PhD student with the group, currently working on extending 
-concurrent separational logics such as TaDA to a total correctness semantics (termination).
+Julian defended his PhD thesis, Compositional termination verification for fine-grained concurrency, in 2022. Julian is currently a Formal Verification Engineer at [Nethermind](https://nethermind.io/), a blockchain company working on Ethereum.

_posts/2021-01-14-world-logic-day.md

@@ -4,7 +4,7 @@ title: UNESCO World Logic Day event
 Philippa Gardner and Petar Maksimovic will take part in the [Computer Science needs Logic!](https://sites.google.com/view/imperial-worldlogicday2021/home) event, part of Imperial College contribution to the [UNESCO World Logic Day](https://en.unesco.org/commemorations/worldlogicday).
 
 The event, organised by Prof Alessandra Russo and Dr Mark Law, wants to 
-celebrate Logic as a vital and core part of Computing. The programme will 
+celebrate Logic as a vital and core part of Computing. The [programme](https://sites.google.com/view/imperial-worldlogicday2021/home/programme) will 
 showcase advancements made in "Logic and Programming Languages" 
 and "Logic and Artificial Intelligence", with presentations by PhD 
 students, post-docs and academics working in areas where there is a 

_posts/2021-04-06-verified.md

+---
+title: Verified software workshops at the Newton institute, May and June
+---
+
+Philippa is one of the organisers of two upcoming workshops on Verification at the [Isaac Newton Institute for Mathematical Sciences]( https://www.newton.ac.uk/), in advance of their scientific programme on [Verified Software](https://www.newton.ac.uk/event/vso), which had to be postponed last summer.
+
+The two workshops: [Verified software: from theory to practice](https://www.newton.ac.uk/event/vsow03), to be held in May, and [Tools and Experiments](https://www.newton.ac.uk/event/vsow04) to be held in June, will be run virtually.  
+
+The workshops are intended for researchers working on the specification and verification of software-intensive systems, with a focus on work bridging the gap between theory and applications.   The Tools and Experiments workshop is aimed at defining an integrated tool resources for automated formal methods with standardized interfaces and it will include a special event marking the 60th anniversary of Tony Hoare's invention of Quicksort.

_posts/2021-04-15-collegedefrance.md

+---
+title: Talk at College de France, Philippa Gardner
+---
+
+Philippa Gardner gave a talk on [Gillian: a Multi-language Platform for Compositional Symbolic Analysis](https://www.college-de-france.fr/site/xavier-leroy/seminar-2021-04-15-11h15.htm) at the [College de France](https://www.college-de-france.fr/site/institution/Le-College-Presentation.htm), as part of their Program logic seminars.
+
+The talk was a  general introduction to [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), a multi-language platform for the development of symbolic-execution tools. Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations that unifies bug catching and verification. So far, the Gillian team has instantiated Gillian to JavaScript and C, languages with substantially different memory models. These instantiations have been used: to find bugs in the real-world data-structure libraries Buckets.js and Collections-C; to find bugs and prove bounded correctness results for a real-world jQuery-like library, cash; and to verify the deserialisation function of the AWS Encryption SDK messaging system.
+
+The video of the talk is available [on this link](https://www.college-de-france.fr/site/xavier-leroy/seminar-2021-04-15-11h15.htm). 

_posts/2021-05-04-pldi21.md

+---
+title: PLDI21 official song and video now out
+---
+
+Another year, another PLDI conference, another excellent PLDI song and video: "Pure Implementation", displaying the musical talents of many friends and colleagues.  
+
+
+<iframe width="560" height="315" src="https://www.youtube.com/embed/77999Td20TM" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe>
+
+
+PLDI is the ACM SIGPLAN Conference on Programming Language Design and Implementation, one of the premier conferences in the field of programming languages and programming systems research. The conference will be held virtually yet again this year, from Sunday 20 to Saturday 26 June 2021. [Registration is now open](https://pldi21.sigplan.org/).

_posts/2021-05-06-talk.md

+---
+title: Public Tech Talk on Gillian Verification of JavaScript and C, Galois
+---
+
+Philippa Gardner gave a public [live-stream](https://youtu.be/DqlC1tNElrg) technical talk on Gillian, Verification of JavaScript and C, hosted by [Galois](https://galois.com/about/). 
+
+The talk gave a general introduction to [Gillian](https://gillianplatform.github.io/), a platform for the development of symbolic-execution tools for many programming languages.
+
+Galois is a company specialising on applying [formal analysis techniques to the design of critical software systems](https://galois.com/research-development/). It runs a program of public [technical talks](https://galois.com/blog/category/tech-talks/), many of which are available online. 

_posts/2021-05-12-sampaio.md

+---
+title: Gabriela Sampaio, internship with the Static Analysis Tools team at Facebook London
+---
+
+Welcome (again) to Gabriela who has returned from her second industry internship, this time a three-months placement with the Static Analysis Tools team at Facebook London.
+
+The team develops [Infer](https://fbinfer.com), an static analysis tool that can find potential bugs in Java/C/C++/Objective-C code. During her internship at Facebook, Gabriela worked on porting [Pulse (an analyser developed as part of Infer)](https://fbinfer.com/docs/checker-pulse) to the Java programming language.

_posts/2021-05-31-cav21.md

+---
+title: Paper accepted at CAV 2021
+---
+
+Congratulations to Petar, Jose, Sacha and Philippa, whose paper and artifact have been accepted to CAV 2021, the [33rd International Conference on Computer-Aided Verification.](http://i-cav.org/2021/)
+
+In their paper, [Gillian, Part II: Real-World Verification for JavaScript and C](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/696e94b1d2bd71031b6933ccac12561d36b38df6/Maksimovic2021Gillian.pdf), they introduce verification based on separation logic to [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), and their methodology for constructing compositional memory models for Gillian. They also verify the JavaScript and C implementations of the [AWS Encryption SDK](https://docs.aws.amazon.com/encryption-sdk/latest/developer-guide/introduction.html) message header deserialisation module, where they found two bugs in the JavaScript and three bugs in the C implementation.
+
+CAV is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems and will be held online this year. 

_posts/2021-06-16-fm21.md

+---
+title: WebAssembly paper accepted
+---
+
+Congratulations to friends and colleagues [Conrad Watt]( https://www.cl.cam.ac.uk/~caw77/), [Xiaojia Rao](https://vtss.doc.ic.ac.uk/people/rao.html), [Jean Pichon-Pharabod](https://www.cl.cam.ac.uk/~jp622/), [Martin Bodin]( https://mbodin.github.io/index.html?pedanticJS=no) and Philippa Gardner, whose paper  [“Two mechanisations of WebAssembly 1.0”](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/d7c1f1ee5690694acefb7f8836dda455ae309b05/Watt2021Two.pdf) has been accepted at the [24th International Symposium of Formal Methods (FM21).](http://lcs.ios.ac.cn/fm2021/)
+
+[WebAssembly (abbreviated Wasm)](https://webassembly.org/) is a new bytecode language supported by all major Web browsers, designed primarily to be an efficient compilation target for low-level languages such as C/C++ and Rust. Wasm is unusual in that it is officially specified through a formal semantics. The paper introduces two mechanised specifications of the WebAssembly 1.0 semantics, written in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. Wasm's compact design and official formal semantics enables the mechanisations to be particularly complete and close to the published language standard. The paper presents a high-level description of the language's updated type soundness result, referencing both mechanisations and also describes the current state of the mechanisation of language features not previously supported: WasmCert-Isabelle includes a verified executable definition of the instantiation phase as part of an executable verified interpreter; WasmCert-Coq includes executable parsing and numeric definitions as on-going work towards a more ambitious end-to-end verified interpreter which does not require an OCaml harness like WasmCert-Isabelle.
+
+FM21, which was planned to take place at the Institute of Software, Chinese Academy of Sciences in Beijing, China on 20-26 2021, will in the end be held online this year.