From 2a3d07881e88186f035e70a3457f920e562db1c2 Mon Sep 17 00:00:00 2001 From: Shale XIONG <shalexiong@dyn1170-15.wlan.ic.ac.uk> Date: Mon, 19 Jun 2017 12:36:53 +0100 Subject: [PATCH] change --- index.md | 6 +++++- publications | 2 +- teaching/InferLab.md | 4 ++-- teaching/ModelsComputation.md | 2 +- teaching/separationlogic.md | 2 +- 5 files changed, 10 insertions(+), 6 deletions(-) diff --git a/index.md b/index.md index 5e2c031..57aed0e 100644 --- a/index.md +++ b/index.md @@ -5,4 +5,8 @@ menu: true menu_order: 1 --- -This research group focuses on mechanised language specification and program verification. We are exploring what it means to build, evaluate, and trust a fully mechanised language specification, using JavaScript as the real-world example language. We are developing library specifications which must be robust with respect to the environment: implementations should not leak; and specifications should be useful to the client. We are developing compositional program reasoning techniques that scale, leading to automatic tools for verifying properties of programs. Our current focus is on reasoning about JavaScript and Concurrency. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course [here](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html). +This research group focuses on mechanised language specification and program verification. +We are exploring what it means to build, evaluate, and trust a fully mechanised language specification, using JavaScript as the real-world example language. +We are developing library specifications which must be robust with respect to the environment: implementations should not leak; and specifications should be useful to the client. +We are developing compositional program reasoning techniques that scale, leading to automatic tools for verifying properties of programs. +Our current focus is on reasoning about JavaScript and Concurrency. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course [here](/teaching/separationlogic.html). diff --git a/publications b/publications index 1b92f81..6f5a6c5 160000 --- a/publications +++ b/publications @@ -1 +1 @@ -Subproject commit 1b92f81b5d4a40cab2150c42035c98c5a5f152e3 +Subproject commit 6f5a6c5d0a76c933312e8bc279d7d61b6a31b881 diff --git a/teaching/InferLab.md b/teaching/InferLab.md index f952cdd..2f04dde 100644 --- a/teaching/InferLab.md +++ b/teaching/InferLab.md @@ -1,7 +1,7 @@ --- title: Separation Logic Infer Lab 2016 -project_id: infer -menu: true +project_id: infe +menu: false parent_menu: Teaching menu_order: 5 sub_menu_order: 2 diff --git a/teaching/ModelsComputation.md b/teaching/ModelsComputation.md index 731e991..39bf43f 100644 --- a/teaching/ModelsComputation.md +++ b/teaching/ModelsComputation.md @@ -1,7 +1,7 @@ --- title: Models of Computation project_id: moc -menu: true +menu: false parent_menu: Teaching menu_order: 5 sub_menu_order: 3 diff --git a/teaching/separationlogic.md b/teaching/separationlogic.md index 475b997..8ebaafa 100644 --- a/teaching/separationlogic.md +++ b/teaching/separationlogic.md @@ -1,7 +1,7 @@ --- title: Separation Logic project_id: sl -menu: true +menu: false parent_menu: Teaching menu_order: 5 sub_menu_order: 1 -- GitLab