diff --git a/blurbs.txt b/blurbs.txt deleted file mode 100644 index 42c7421b1317a66ba4dbc1b3eb50a5d94d4edb6c..0000000000000000000000000000000000000000 --- a/blurbs.txt +++ /dev/null @@ -1,6 +0,0 @@ -The world-wide web is a nearly-ubiquitous and continuously-growing application platform. -As users increasingly come to depend on web applications, it is more important than ever to be able to make guarantees about these programs. -Yet these applications are built on a melange of technologies that have evolved in response to the demands of developers and users, which present a daunting task for formal analysis. - -The purpose of the Reliable Web group is to develop formal techniques for making guarantees about web applications. -Particular successes include formalising the semantics of JavaScript, the dynamic language that underpins client-side web applications, and developing local reasoning about the W3C Document Object Model, the data model that web applications use to represent and manipulate web documents. \ No newline at end of file diff --git a/research/concurrency.md b/research/concurrency.md index 722c57c58baf85984d3a15be1d6aac10e6030d77..af9fb659913d3c8f6dcf36256f3c767d5c558a3d 100644 --- a/research/concurrency.md +++ b/research/concurrency.md @@ -27,7 +27,7 @@ logics, and applying our work to real-world concurrent programs. This research is supported by the EPSRC programme grant [EP/K008528/1]: [REMS: Rigorous Engineering of Mainstream -Systems][REMS] and the EPSRC programme grant [EP/H008373/2]: [Resource +Systems][REMS] and previously by the EPSRC programme grant [EP/H008373/2]: [Resource Reasoning]. We also have substantial collaboration with [Thomas Dinsdale-Young], previously a PhD student and RA of Gardner and now an independent research fellow at the University of Aarhus. diff --git a/research/javascript.md b/research/javascript.md index 28b50057b951e3b02280c90df926fe9590722007..951d7cbded375e8f2bad10ffb119ced557d1c083 100644 --- a/research/javascript.md +++ b/research/javascript.md @@ -40,13 +40,18 @@ JSIL to develop front-ends for the CBMC and Infer verification tools. #### Research Support This research is supported by the EPSRC/GCHQ grant [EP/K032089/1]: -[Certified Verification of Client-Side Web Programs][1] and the EPSRC -programme grant [EP/H008373/2]: [Resource Reasoning]. We also -interact extensively with [Arthur Charguéraud], [Alan Schmitt] and +[Certified Verification of Client-Side Web Programs][1], the EPSRC +programme grant [EP/K008528/1]: [REMS: Rigorous Engineering of +Mainstream Systems][REMS] and previously by the EPSRC +programme grant [EP/H008373/2]: [Resource Reasoning]. + +We also interact extensively with [Arthur Charguéraud], [Alan Schmitt] and [Martin Bodin] of INRIA, who are supported by the [AJACS] project. [EP/K032089/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K032089/1 [EP/H008373/2]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/H008373/2 +[EP/K008528/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K008528/1 +[REMS]: http://www.cl.cam.ac.uk/~pes20/rems/ [1]: https://verificationinstitute.org/project/certified-verification-of-client-side-web-programs/ [Resource Reasoning]: http://www.resourcereasoning.com/ [Arthur Charguéraud]: http://www.chargueraud.org/