blurbs

_research/concurrency.md

@@ -3,17 +3,19 @@ title: Concurrency
 project_id: concurrency
 ---
 
-Concurrent programs and libraries are ubiquitous in today's world of multi-core processor architectures, 
-and the need for reasoning about concurrent programs and verifying their correctness grows 
-increasingly more important. These research problems are still considered difficult for a variety of reasons,
-such as the fact that we need to consider and reach conclusions about a shared state 
-affected by multiple threads, or that we require effective abstractions for describing the complex behaviour created by multiple threads.
+We develop formal reasoning techniques for concurrent programs, with a
+particular emphasis on concurrent program logics. Recently, various
+logics based on separation logic have been developed, by ourselves and
+others, to provide more modular reasoning about concurrent programs.
+Our work has tackled a range of problems including data abstraction,
+abstract atomicity, fault-tolerance and progress. In particular, we
+have recently developed {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, {% cite_details Dinsdale-Young2013Views --text Views %}, {% cite_details daRochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details daRochaPinto2016Modular --text Total-TaDA %}.
 
-Our research agenda is to develop formal reasoning methods about concurrency with a focus on concurrent program logics.
-Recently, various logics based on separation logic were introduced with the aim of verifying functional correctness of fine-grained concurrent programs.
-We have played a significant role in the development of {% cite_details Dinsdale-Young2010Concurrent --text Concurrent Abstract Predicates %}, {% cite_details Dinsdale-Young2013Views --text Views %}, {% cite_details daRochaPinto2014TaDA --text TaDA %}, {% cite_details Raad2015CoLoSL --text CoLoSL %}, {% cite_details Ntzik2015Fault --text Fault-tolerant Concurrent Separation Logic %} and {% cite_details daRochaPinto2016Modular --text Total-TaDA %}.
-These logics have tackled a range of problems, including data abstraction, atomicity abstraction, fault-tolerance, terminal, while introducing more modular and compositional ways to reason about concurrent programs.
-We have applied these logics to the verification of large problems, such as data structures used in databases and java.util.concurrent, as well as the specification of file systems.
-
-Our mission is to continually challenge and improve the state-of-the-art, targeting progress properties, specification of concurrency in POSIX filesystems, refinement of our logics so that we can deal with more advanced algorithms, and the development of automated reasoning tools based on these logics.
+We have applied our  reasoning to, for example, algorithms for
+manipulating concurrent B-trees,  skip lists from
+java.util.concurrent, graph algorithms and the POSIX file system.
+Our goal is to challenge and improve the state-of-the-art in
+concurrent reasoning, refining our logics to deal with more advanved
+concurrent programs, developing automated reasoning tools based on these
+logics, and applying our work to real-world concurrent programs.
 

_research/javascript.md

@@ -3,3 +3,36 @@ title: JavaScript
 project_id: javascript
 ---
 
+We study the mechanised specification of the JavaScript language
+(following the ECMAScript 5 standard) and the verification of
+JavaScript programs.
+
+<h4>JSCert</h4>
+
+With Bodin, Charguéraud, and Schmitt at INRIA, we
+have developed <a href="http://jscert.org/">JSCert</a>, a substantial Coq specification that is
+line-by-line close to the core language of the ECMAScript 5
+standard. It comes with a reference interpreter, JSRef, proven correct
+with respect to JSCert and tested using the official Test262 test
+suite. We are currently extending this specification to the
+numerous libraries, providing continuous test integration for the
+ever-growing specification, developing a new, human-readable JSRef,
+with a tighter connection to the standard and good tracking
+properties, and creating the web service Explain.js to explain
+behavioural complexities of JavaScript programs.
+
+<h4>JSIL</h4>
+
+We have developed a principled compiler from JavaScript (ECMAScript 5
+strict) to a small intermediate language JSIL, which has a simpler
+operational semantics and is better suited to program verification.
+The compiler has been substantially tested using the Test262 test
+suite and it comes with a hand-proof of translation correctness 
+for a fragment of the language. We will use JSIL to develop JSVerify - a
+verification tool for JavaScript. Daiva Naudžiūnienė will
+this year hold internships at Amazon and Facebook  to use
+JSIL to develop front-ends for the CBMC and Infer verification tools.
+
+<h4>Research Support</h4>
+
+To be added...
\ No newline at end of file

index.md

@@ -4,5 +4,6 @@ title: Home
 menu: true
 menu_order: 1
 ---
-One paragraph about the group and its research, about 4 lines of text would be good here. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Ut ante enim, bibendum vitae vestibulum in, luctus et diam. Quisque pulvinar accumsan nisl, et lobortis enim euismod quis. Praesent pulvinar nulla justo, ut vulputate leo blandit sit amet. Mauris fringilla sodales nulla at porta. Vivamus ligula leo, ultrices ut quam sit amet, ullamcorper volutpat magna. Quisque consequat, sem in lobortis scelerisque, quam turpis ornare odio, auctor congue nisi velit in dolor. Curabitur auctor fermentum eros at dictum.
+
+This research group focusses 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 reasoning techniques that scale, leading to automatic tools for verifiying properties of programs. Our current main focus is on program specification and verification for JavaScript and Concurrency.
 

research.md

@@ -4,7 +4,7 @@ menu: true
 menu_order: 2
 ---
 
-Details about the group's research, more than on the homepage. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Ut ante enim, bibendum vitae vestibulum in, luctus et diam. Quisque pulvinar accumsan nisl, et lobortis enim euismod quis. Praesent pulvinar nulla justo, ut vulputate leo blandit sit amet. Mauris fringilla sodales nulla at porta. Vivamus ligula leo, ultrices ut quam sit amet, ullamcorper volutpat magna. Quisque consequat, sem in lobortis scelerisque, quam turpis ornare odio, auctor congue nisi velit in dolor. Curabitur auctor fermentum eros at dictum.
+The main focus of our group is on program specification and verification for JavaScript and Concurrency.
 
 {% for item in site.research %}
 <h3><a href="{{ item.url }}">{{ item.title }}</a></h3>