.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/gardner.md

@@ -32,4 +32,4 @@ 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', 2021](http://www.newton.ac.uk/event/vso). 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).
+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.
+Petar is also a Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.
\ No newline at end of file

_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.
+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

_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-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-31-cav21.md

@@ -4,6 +4,6 @@ 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, 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.
+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

@@ -2,7 +2,7 @@
 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” has been accepted at the [24th International Symposium of Formal Methods (FM21).](http://lcs.ios.ac.cn/fm2021/)
+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.
 

_posts/2021-07-01-toplas.md 1.83 KB → _posts/2021-07-02-toplas.md

 ---
 title: Paper accepted at TOPLAS
 ---
-
 Many congratulations to [Emanuele D’Osualdo](https://www.emanueledosualdo.com/about/), [Azadeh Farzan](https://www.cs.toronto.edu/~azadeh/), Philippa Gardner and [Julian Sutherland](https://www.doc.ic.ac.uk/~jhs110/), whose paper [“TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs”](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/d7c1f1ee5690694acefb7f8836dda455ae309b05/DOsualdo2020TaDa.pdf) has been accepted for publication at the [ACM Transactions on Programming Languages and Systems (TOPLAS)](https://dl.acm.org/journal/toplas) journal. 
 
-The paper introduces TaDA Live, a separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The logic contributes several innovations to obtain modular rely/guarantee style reasoning for liveness properties and to blend them with logical atomicity.  
+The paper introduces TaDA Live, a separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The logic contributes several innovations to obtain modular rely/guarantee style reasoning for liveness properties and to blend them with logical atomicity. 
 
-TOPLAS is the bimonthly ACM peer-reviewed scientific journal on programming languages. TOPLAS reports in depth on recent research advances in the areas of programming languages. Papers published must have content that is innovative, novel and advances the art of programming languages and systems.
+TOPLAS is the bimonthly ACM peer-reviewed scientific journal on programming languages. TOPLAS reports in depth on recent research advances in the areas of programming languages. Papers published at TOPLAS must contain innovative and novel content that advances the state of the art of programming languages and systems; many congratulations to all on a fine achievement after a lot of hard work.

_posts/2021-08-14-ara.md

+---
+title: Amazon Research Award (ARA) to Philippa Gardner
+---
+
+Philippa Gardner has been announced as one of the recipients of the [Spring 2021 Amazon Research Awards (ARA)](https://www.amazon.science/research-awards).
+
+ARA is a program funding academic research to open-source projects by top academic researchers around the world. Philippa was one of 26 awards made to researchers from 25 universities in 11 countries. Her successful proposal: Gillian: A Multi-language Platform for Symbolic Testing and Verification, was funded as part of ARA's Amazon Web Services Automated Reasoning call. 
+
+[Daniel Kroening, senior principal scientist for the Automated Reasoning Group](https://www.amazon.science/author/daniel-kroening), welcomed the new ARA researchers. "Research in automated reasoning is deeply intertwined with a broad range of other research areas, touching machine learning, hardware and software engineering, robotics, and life sciences," he said "The 2021 Amazon Research Awards reflect this breadth, and the interdisciplinary nature of research that is necessary to take computing one step closer to that magic spark that drives human reasoning."   
+
+The proposed work, to instantiate Gillian with Rust and to test and verify some of the unsafe code in the standard Rust library, is part of the goal to develop Gillian into a robust platform for symbolic testing and verification, usable by specialist tool developers, professional code developers, and students.

_posts/2021-09-03-caroline.md

+---
+title: Welcome to Caroline Cronjager, visiting student
+---
+
+We are very happy to welcome Caroline Cronjager, a visiting student from Ruhr University Bochum, Germany.
+
+Caroline is a BSc Mathematics with Computer Science student from Ruhr-University Bochum, Germany. During the next three months she plans to
+work on incorrectness and under-approximating logic, starting off with soundness for under-approximate separation logic and will also be part of the team supporting students on the Scalable Software Verification course.  

_posts/2021-10-03-andreas.md

+---
+title: Welcome to Andreas Lööw, new researcher with the group
+---
+
+A very warm welcome to Andreas Lööw, who has just started with us as a Post-Doctoral researcher. 
+
+Andreas completed his PhD on [Building Verified Hardware and Verified Stacks in HOL](https://www.doc.ic.ac.uk/~aloow/papers/thesis.pdf) at Chalmers University of Technology, under the supervision of [Magnus Myreen](http://www.cse.chalmers.se/~myreen/). 
+
+[Andreas' research focuses on interactive theorem proving for software and hardware correctness](https://www.doc.ic.ac.uk/~aloow/) and much of his work revolves around trustworthy hardware; [his latest paper, on the development and verification of the Verilog synthesis tool Lutsig](https://dl.acm.org/doi/10.1145/3437992.3439916) was accepted at this year’s POPL’s [Certified Programs and Proofs (CPP)]( https://popl21.sigplan.org/home/CPP-2021?.) series.

_posts/2021-11-01-sacha_amazon.md

+---
+title: Sacha Ayoun, internship with Amazon Web Services
+---
+
+Welcome back to Sacha who has returned from a three-months internship with the CodeGuru team at Amazon Web Services.
+
+Amazon CodeGuru is a [set of publicly available developer tools](https://aws.amazon.com/codeguru/) that use machine learning to automatically review code for bugs and code quality and to suggest improvements.
+
+While at AWS, Sacha developed a proof of concepts analysis for Java that could help reduce the number of false positives or reduce the search space in other kinds of analyses without compromising soundness. Having enjoyed his time at AWS, he is planning to return for a second internship with them next year.

_posts/2021-11-05-his.md

+---
+title: Philippa Gardner, talk at High Integrity Software (HIS) conference
+---
+
+Philippa gave a talk on [Verified Trustworthy Software Specification](https://www.his-conference.co.uk/index.php?p=session/verified-trustworthy-software-systems) at this year's [High Integrity Software (HIS) Conference](https://www.his-conference.co.uk/).
+
+Now in its sixth year, [HIS](https://www.his-conference.co.uk/index.php?p=programme) aims to create a forum to share challenges, best practice and experience between software engineering practitioners. This year's HIS conference, under the theme: Assuring security and safety for critical software applications, focussed on cyber safety for embedded systems, innovations in testing and the application of formal methods to achieve cyber security.