diff --git a/_people/ayoun.md b/_people/ayoun.md
index 1dd8cd5d5a6b7eb090e67a8819dee88949cfb3db..1fe8707ca3f9d5ae6c80292b572968a03d45bcf9 100644
--- a/_people/ayoun.md
+++ b/_people/ayoun.md
@@ -8,7 +8,7 @@ github: https://github.com/Giltho/
alumnus: false
projects:
- gillian
- - moc
+ - sl
---
Sacha Ayoun is a PhD student at the Department of Computing at Imperial, under
the supervision of Professor Philippa Gardner. During his undergraduate 2017,
diff --git a/_people/fragoso-santos.md b/_people/fragoso-santos.md
index e535d8c5487c19bbcb5d6c4f4bc5b82f0a62f261..74362d630f39657a0b6e206bcbe5497375e7bd8b 100644
--- a/_people/fragoso-santos.md
+++ b/_people/fragoso-santos.md
@@ -6,11 +6,6 @@ webpage: http://web.ist.utl.pt/jose.fragoso/
email: jose.fragoso@tecnico.ulisboa.pt
github: j3fsantos
alumnus: true
-projects:
- - web
- - sl
- - infer
- - gillian
---
José joined the group as a Research Associate in 2015, working on
diff --git a/_people/raad.md b/_people/raad.md
index a32f5c38aa84a8472c480932a87742cbab741f4f..e2731a6828168b24146ab94070069fed51785b25 100644
--- a/_people/raad.md
+++ b/_people/raad.md
@@ -8,7 +8,7 @@ alumnus: true
---
Azalea was a PhD student with the group, defending her thesis on [Abstraction, Refinement and Concurrent Reasoning]({{site.baseurl}}{% link publications/Raad2017Abstraction.html %}) in February 2017.
-She then moved to the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/)
+She then moved to the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/)
working a postdoctoral researcher with [Derek Dreyer](https://people.mpi-sws.org/~dreyer/) and [Viktor Vafeiadis](https://people.mpi-sws.org/~viktor/)
-on the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/). In 2020 Azalea joined the faculty
+on the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/). In 2020, Azalea joined the faculty
at Imperial College London as a lecturer.
\ No newline at end of file
diff --git a/_people/wood.md b/_people/wood.md
index 538490c26b1976a7368249be84a9b6e6e5d878cc..b63efe21c1f2f4b6615bcec58233ee8b71a7de50 100644
--- a/_people/wood.md
+++ b/_people/wood.md
@@ -5,8 +5,6 @@ position: PhD Student
webpage: https://twitter.com/IgnoredAmbience
github: IgnoredAmbience
alumnus: true
-projects:
- - web
---
Thomas was a PhD student with the group, working on software automated testing, verification and reasoning techniques and theory.
\ No newline at end of file
diff --git a/research/javascript.md b/research/javascript.md
index 27ab7203541afe0565570460426e0ab96fc32313..8f519820f2394597715f6448182564bef33648e6 100644
--- a/research/javascript.md
+++ b/research/javascript.md
@@ -15,22 +15,19 @@ We are also interested in the mechanised specification of JavaScript itself.
We have developed JaVerT, a compositional symbolic analysis tool for JavaScript, targeting the strict mode of the ECMAScript 5 standard. JaVerT supports whole-program symbolic testing, verification and automatic compositional testing based on bi-abduction. It comprises:
-—JSIL, an intermediate goto language with a symbolic execution engine with explicit management of execution errors that guides the feedback for symbolic testing and the automatic bi-abductive inference. The meta-theory underpinning JSIL is formally defined and modular, streamlining the proofs and guiding the implementation.
-
-—JS-2-JSIL, a trusted compiler that preserves the JavaScript memory model and semantics, trusted in the sense that it is line-by-line close to the standard and comprehensively tested using the official Test262 test suite.
+— JSIL, an intermediate goto language with a symbolic execution engine with explicit management of execution errors that guides the feedback for symbolic testing and the automatic bi-abductive inference. The meta-theory underpinning JSIL is formally defined and modular, streamlining the proofs and guiding the implementation.
+— JS-2-JSIL, a trusted compiler that preserves the JavaScript memory model and semantics, trusted in the sense that it is line-by-line close to the standard and comprehensively tested using the official Test262 test suite.
#### Web APIs
Using our considerable experience with the DOM specification and JavaScript analysis, we have recently (ECOOP'20) introduced a trusted infrastructure for symbolic analysis of modern event-driven Web applications, comprising:
-—reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises, and the JavaScript async/await APIs, all following the API standards as closely as possible and all thoroughly tested against the official test suites;
-
-—a simple Core Events Semantics that is sufficiently expressive to describe the event models underlying these APIs;
-
--JaVerT.Click, an extension of JaVerT with the Core Events Semantics, that is, for the first time, able to symbolically test JavaScript programs that use any/all of the above-mentioned APIs.
+— reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises, and the JavaScript async/await APIs, all following the API standards as closely as possible and all thoroughly tested against the official test suites;
+— a simple Core Events Semantics that is sufficiently expressive to describe the event models underlying these APIs;
+- JaVerT.Click, an extension of JaVerT with the Core Events Semantics, that is, for the first time, able to symbolically test JavaScript programs that use any/all of the above-mentioned APIs.
-We have used JaVerT.Click to analyse the events module of [cash][https://kenwheeler.github.io/cash/], a small, widely-used jQuery alternative, in which we found two bugs (fixed) and for which we have proven boundned correctness of several essential properties, such as "an event handler can be triggered if and only if it has previously been registered".
-We have also found a bug in the [p-map][https://github.com/sindresorhus/p-map] library (fixed), which extends the functionality of JavaScript Promises.
+We have used JaVerT.Click to analyse the events module of [cash](https://kenwheeler.github.io/cash/), a small, widely-used jQuery alternative, in which we found two bugs (fixed) and for which we have proven boundned correctness of several essential properties, such as "an event handler can be triggered if and only if it has previously been registered".
+We have also found a bug in the [p-map](https://github.com/sindresorhus/p-map) library (fixed), which extends the functionality of JavaScript Promises.
#### Language Semantics