diff --git a/_posts/2016-07-26-advert.md b/_posts/2016-07-26-advert.md index acbeaa71813228d7280bd984187e5bc5e3cd8b16..fca2adbe1926e9776d8080f0bfd7244593d50864 100644 --- a/_posts/2016-07-26-advert.md +++ b/_posts/2016-07-26-advert.md @@ -3,13 +3,13 @@ title: One new postdoc position at Imperial College --- We are looking to recruit one postdoctoral researcher in the Program Specification and Verification Group at Imperial College London, to work on reasoning about concurrent programs. The position is suitable for either a theoretician, who would work on the foundations of concurrent reasoning, or a theoretician/practitioner, who would work on the verification and testing of file systems. -<b> \*\*\* Deadline: 18th September \*\*\* </b> +<b> \*\*\* Applications now closed \*\*\* </b> This position will have an initial duration of 2.5 years, with a certain level of flexibility with respect to the start date and possible extensions. It will be funded as part of the £5.6M EPSRC Programme Grant ["REMS: Rigorous Engineering of Mainstream Systems"](https://www.cl.cam.ac.uk/~pes20/rems/index.html), at the University of Cambridge, University of Edinburgh, and Imperial College London The Department of Computing at Imperial provides a vibrant and stimulating research environment in the heart of London, with leading research groups working on programming languages, verification, and testing. The quality of the Department has been consistently awarded the highest research and teaching rating. In the latest Research Excellence Framework assessment of 2014, the Department was ranked third (first in the Research Intensity table published by the Times Higher). In addition, at the last national assessment of teaching quality, the Department was rated as "Excellent" and came 2nd in The Complete University Guide, The Guardian, The Times and The Sunday Times national league tables by subject. -The Program Specification and Verification Group is led by Professor Philippa Gardner, and its current focus is on reasoning about JavaScript and concurrency. The advertised position will target concurrency in particular (see http://psvg.doc.ic.ac.uk/research/concurrency.html). The breadth of the REMS project allows for flexibility in the profile of the candidate, who would work either on the foundations of concurrency reasoning or on the verification and testing of file systems. +The Program Specification and Verification Group is led by Professor Philippa Gardner, and its current focus is on reasoning about JavaScript and concurrency. The advertised position will target [concurrency](/research/concurrency.html) in particular. The breadth of the REMS project allows for flexibility in the profile of the candidate, who would work either on the foundations of concurrency reasoning or on the verification and testing of file systems. <b> \*\*\* Foundations of concurrency reasoning \*\*\* </b> Recently, various program logics based on concurrent separation logic have been developed, by ourselves and others, with the aim of providing more modular abstract reasoning about concurrent programs. Our work at Imperial has tackled a range of problems, including data abstraction (Concurrent Abstract Predicates), abstract atomicity (the TaDA logic), fault-tolerance and progress, applying our reasoning to concurrent B-trees, skip lists from java.util.concurrent, graph algorithms, and the POSIX file system. The advertised position is suitable for someone interested in such foundational work on concurrency reasoning and, in particular, its relationship with respect to linearisability. diff --git a/_posts/2016-09-01-newmember.md b/_posts/2016-09-01-newmember.md index 018c5dcc090cb1c85dac2231168dda2d74e8276d..a5d8d5165a388076a6bf439c562f6ba3e15b69fe 100644 --- a/_posts/2016-09-01-newmember.md +++ b/_posts/2016-09-01-newmember.md @@ -5,6 +5,6 @@ We are very happy to welcome Andrea Cerone to the group. Andrea has joined us fr Andrea is currently working on frameworks for specifying weak consistency models of geo-replicated databases and applications of transaction chopping for various consistency models. Andrea did his Ph.D at Trinity College Dublin with Prof Matthew Hennessy, so he claims to be quite unfazed by the UK weather. -You can find more about Andrea on [his webpage](https://www.doc.ic.ac.uk/~acerone/) +You can find more about Andrea on [his webpage](https://www.doc.ic.ac.uk/~acerone/). diff --git a/_posts/2016-10-03-papers.md b/_posts/2016-10-03-papers.md index c222fd8e7e72c86a0dbd1c73c32bb7ed0134077b..b24299da7ec9ecfdb35f3ec8a5ccb2a75a6f3a37 100644 --- a/_posts/2016-10-03-papers.md +++ b/_posts/2016-10-03-papers.md @@ -3,5 +3,6 @@ title: Papers published by Azalea Raad --- Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, [APLAS 2016](https://soict.hust.edu.vn/~aplas2016/). -The papers are: [Verifying Concurrent Graph Algorithms](http://psvg.doc.ic.ac.uk/publications/Raad2016Verifying.html) (with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://psvg.doc.ic.ac.uk/publications/Raad2016DOM.html) (with José Fragoso Santos and Philippa Gardner) -These and other group papers can be found on our [publications page](http://psvg.doc.ic.ac.uk/publications/) +The papers are: [Verifying Concurrent Graph Algorithms](http://psvg.doc.ic.ac.uk/publications/Raad2016Verifying.html) (with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://psvg.doc.ic.ac.uk/publications/Raad2016DOM.html) (with José Fragoso Santos and Philippa Gardner). + +These and other group papers can be found on our [publications page](http://psvg.doc.ic.ac.uk/publications/). diff --git a/_posts/2016-11-23-dagstuhl.md b/_posts/2016-11-23-dagstuhl.md index 37cd178cb81cb9101c148ec5acd91384e57fd24f..4f3536baf9faa3c8bbf5246f58c8296bf9105e58 100644 --- a/_posts/2016-11-23-dagstuhl.md +++ b/_posts/2016-11-23-dagstuhl.md @@ -8,4 +8,4 @@ Andrea Cerone was invited to attend the seminar on [Concurrency with Weak Memory The seminar covered a wide range of topics, including fundamental results in the theory underlying weak memory models, applications in the fields of hardware architectures, compiler optimisations and transactional systems, -as well as static analysis techniques for the analysis of programs. Andrea Cerone gave a talk on ‘Analyzing Snapshot Isolation’ +as well as static analysis techniques for the analysis of programs. Andrea Cerone gave a talk on 'Analyzing Snapshot Isolation'. diff --git a/_posts/2016-12-15-Dolby.md b/_posts/2016-12-15-Dolby.md index e0745d305a0df2efe04886c04cb063cceaf0f748..fa434990fb5ededf99fdf7d86199c43e8645ec0d 100644 --- a/_posts/2016-12-15-Dolby.md +++ b/_posts/2016-12-15-Dolby.md @@ -3,10 +3,12 @@ title: Visit from Julian Dolby, IBM --- [Julian Dolby](http://researcher.watson.ibm.com/researcher/view.php?person=us-dolby), a researcher at IBM's [Thomas J. Watson Research Center](http://www.research.ibm.com/labs/watson/index.shtml) -in New York visited the PSVG group for a week in December. Julian’s research focuses on static program analysis, +in New York visited the PSVG group for a week in December. + +Julian’s research focuses on static program analysis, software testing and the semantic web and during his visit, Julian worked with José Fragoso and Petar Maksimovic in a [symbolic analysis for JavaScript](https://psvg.doc.ic.ac.uk/research/javascript.html) based on JSIL and Rosette with the end goal of having a bug-finding tool for JavaScript. [ROSETTE](https://github.com/juliandolby/rosette) is a solver-aided programming language -that extends Racket with language constructs for program synthesis, verification, and more. \ No newline at end of file +that extends Racket with language constructs for program synthesis, verification, and more. diff --git a/_posts/2017-01-13-Pedro_viva.md b/_posts/2017-01-13-Pedro_viva.md index 44445c8b9a53c6746a4ecc0aa8b9cc2cc7d30f49..2c4884cefeaab11087fcdd7d447a2241fbf4da73 100644 --- a/_posts/2017-01-13-Pedro_viva.md +++ b/_posts/2017-01-13-Pedro_viva.md @@ -9,5 +9,6 @@ and to [Susan Eisenbach](http://www.imperial.ac.uk/people/s.eisenbach), who acte Pedro’s thesis was about exploring a number of design possibilities for a logic for modularly verifying shared-memory concurrent programs and introduces a new program logic -called [TaDA](https://psvg.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html) for verifying concurrent programs with much better support for abstraction -The latest paper from Pedro, accepted to ESOP 2017 is on [our publications page](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html) +called [TaDA](https://psvg.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html) for verifying concurrent programs with much better support for abstraction. + +Pedro's latest paper, accepted to ESOP 2017 is on [our publications page](https://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html). diff --git a/_posts/2017-02-01-Gian_viva.md b/_posts/2017-02-01-Gian_viva.md index 3afaf1e5c51ccb98fa539a2e25a7e0c34e796097..d3df0e3435a7ca873e18d49459086477b2c1b22c 100644 --- a/_posts/2017-02-01-Gian_viva.md +++ b/_posts/2017-02-01-Gian_viva.md @@ -12,4 +12,4 @@ clients that interact with the API. The examiners found that Gian’s work conta on formal specification and verifications of concurrent software systems and recommended that the viva is passed with only minor corrections. -More details on Gian’s research can be found [here](https://psvg.doc.ic.ac.uk/people/ntzik.html) +More details on Gian’s research can be found [here](https://psvg.doc.ic.ac.uk/people/ntzik.html). diff --git a/_posts/2017-02-11-INVEST.md b/_posts/2017-02-11-INVEST.md index b5eca5c8f27f78fd394d4f89f6ee66cdd7e92407..c502ddef12f8e30c5c7c3791aade9fcb7fcb3e04 100644 --- a/_posts/2017-02-11-INVEST.md +++ b/_posts/2017-02-11-INVEST.md @@ -13,8 +13,8 @@ look at the fields of [software verification and testing](http://wp.doc.ic.ac.uk During the all day workshop, students were able to listen to and engage with world-leading academic scholars, experience what it is like being a Verification and Testing researcher, and network with other students and current Post-Docs. -There were a number of talks, including one on How to Give Talks That People Can Follow, +There were a number of talks, including one on "How to Give Talks That People Can Follow", by [Derek Dreyer](https://people.mpi-sws.org/~dreyer/), of the [Max Planck Institute for Software Systems (MPI-SWS), Germany]( https://www.mpi-sws.org/) and one minute presentations by students. - \ No newline at end of file + diff --git a/_posts/2017-02-14-NCSC_official_opening.md b/_posts/2017-02-14-NCSC_official_opening.md index 0c42827e9e0005c7621e22d275d569d327618e0c..be962a77f836ae0e37c57af0abaf2196c3ffa8b0 100644 --- a/_posts/2017-02-14-NCSC_official_opening.md +++ b/_posts/2017-02-14-NCSC_official_opening.md @@ -1,15 +1,15 @@ --- title: National Cyber Security Centre (NCSC) official opening --- -Philippa Gardner attended the official opening by the Queen of the [National Cyber Security Centre](https://www.ncsc.gov.uk/) new headquarters in London. +Philippa Gardner attended the official opening by the Queen of the [National Cyber Security Centre](https://www.ncsc.gov.uk/)'s new headquarters in London. The NCSC, part of GCHQ, aims to make their work on cyber security more open; it will publish research, organise events and will provide advice on cyber security to businesses and members of the public. Philippa was introduced to the Queen and spoke to her and Prince Philip about her role as director of the new Research Institute on Verified Trustworthy Software Systems (VeTSS). -For details of the opening and a photo of the Queen see the [BBC news page on the opening](http://www.bbc.co.uk/news/uk-38964996) +For details of the opening and a photo of the Queen see the [BBC news page on the opening](http://www.bbc.co.uk/news/uk-38964996). -You can also check the [NCSC blog](https://www.ncsc.gov.uk/blog-post/how-ncsc-built-its-own-it-system) for details on how they built their IT system. +You can also check the [NCSC blog](https://www.ncsc.gov.uk/blog-post/how-ncsc-built-its-own-it-system) for details on how they built their IT system. diff --git a/_posts/2017-04-24-Dosualdo.md b/_posts/2017-04-24-Dosualdo.md index c75f89fd3793c6e4701529b4e002fc0c36f3a5c3..6ab52a01c796529116f6674a28dd376e6159e502 100644 --- a/_posts/2017-04-24-Dosualdo.md +++ b/_posts/2017-04-24-Dosualdo.md @@ -9,4 +9,4 @@ at the University of Oxford under the supervision of Prof Luke Ong, winning the Emanuele joins us from the [Concurrency Theory Group at the University of Kaiserslautern]( http://concurrency.cs.uni-kl.de/), Germany where he worked with [Prof Roland Meyer]( http://concurrency.cs.uni-kl.de/group/meyer/home.html). His current work focuses on models of concurrent behaviour to enable the construction of automatic analyses for concurrent systems. -More details on his [webpage:](http://www.emanueledosualdo.com/research/) +More details on his [webpage](http://www.emanueledosualdo.com/research/). diff --git a/_posts/2017-05-03-consistency.md b/_posts/2017-05-03-consistency.md index 08814209221a9933b3a4c0f5c36dfd72cbb16f9e..4cb0a5594285a8cf1ca1cc550810ec29df2eafa4 100644 --- a/_posts/2017-05-03-consistency.md +++ b/_posts/2017-05-03-consistency.md @@ -1,15 +1,13 @@ --- title: Philippa Gardner, talk at the open Workshop on Consistency in Distributed Storage Systems, LIP6, Paris --- -Philippa Gardner gave at talk on A Concurrent Specification of PoSIX at the open workshop [“Consistency in distributed storage.â€](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/) +Philippa Gardner gave a talk on "A Concurrent Specification of PoSIX" at the open workshop "[Consistency in distributed storage](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/)". organised by [Marc Shapiro](https://pages.lip6.fr/Marc.Shapiro/) [(UPMC-LIP6 and Inria)](https://www.inria.fr/). - - This year's workshop, held at the Université Pierre et Marie Curie - LIP6, Paris, France on 3 May 2017, offered students and academics an opportunity to share insights on the principles and practice of distributed data replication systems, based on solid distributed algorithm and engineering principles. The workshop is held under the aegis of the French ANR Project RainbowFS, which aims to deconstruct consistency and to develop principled tools for the design, verification, deployment and monitoring, and to use them for developing a correct-by-construction and efficient geo-scale petabyte-sized storage system. -Philippa’s abstract and slides are available on the [workshop page](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/). \ No newline at end of file +Philippa’s abstract and slides are available on the [workshop page](https://pages.lip6.fr/Marc.Shapiro/workshop-2017-05-03/). diff --git a/_posts/2017-05-08-aarhus.md b/_posts/2017-05-08-aarhus.md index a2e39dc14d8eee3e87e69ab7ced764844ff6f0f4..1c42be9b1d5f26c7fe53506f02154c3c312b445c 100644 --- a/_posts/2017-05-08-aarhus.md +++ b/_posts/2017-05-08-aarhus.md @@ -12,6 +12,6 @@ is the latest in a series previously held at [University of Kent](https://www.cs [Imperial College London](http://multicore.doc.ic.ac.uk/icw2015/), [The University of York](https://www-users.cs.york.ac.uk/~miked/ycw2014/), [University of Oxford](http://www.cs.ox.ac.uk/people/hongseok.yang/ccw12/index.html), [Trinity College Dublin](https://www.scss.tcd.ie/Vasileios.Koutavas/dcw2011/), [Cambridge University](https://www-users.cs.york.ac.uk/~miked//ccw2010/index.html), Newcastle, -and [Queen Mary}(https://web.archive.org/web/20100606005049/http://www.eecs.qmul.ac.uk/~ohearn/Workshops/Concurrency09/). +and [Queen Mary](https://web.archive.org/web/20100606005049/http://www.eecs.qmul.ac.uk/~ohearn/Workshops/Concurrency09/). -Aarhus is the second largest city in Denmark and is one of the 2017 [European Capitals of Culture](http://www.aarhus2017.dk/en/). \ No newline at end of file +Aarhus is the second largest city in Denmark and is one of the 2017 [European Capitals of Culture](http://www.aarhus2017.dk/en/). diff --git a/_posts/2017-06-13-csf.md b/_posts/2017-06-13-csf.md index 6f89b2a4f368c4420ae32d7bfb33d9dc32a4bca5..09817ed2a5d7f0adecb01a953f0ffae0314bc40e 100644 --- a/_posts/2017-06-13-csf.md +++ b/_posts/2017-06-13-csf.md @@ -4,7 +4,7 @@ title: Paper accepted at CSF'17 Emanuele D'Osualdo has had a paper accepted at this year's [Computer Security Foundations Symposium (CSF)](http://csf2017.tecnico.ulisboa.pt/index.html). Emanuele's paper, in collaboration with [Luke Ong](http://www.cs.ox.ac.uk/luke.ong/), University of Oxford, UK and [Alwen Tiu](http://www.ntu.edu.sg/home/atiu/), -Nanyang Technological University, Singapore, is entitled ['Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes'](http://www.emanueledosualdo.com/research/papers/2017/csf-decidable-secrecy.html) +Nanyang Technological University, Singapore, is entitled ['Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes'](http://www.emanueledosualdo.com/research/papers/2017/csf-decidable-secrecy.html). In the paper, the authors introduce a new class of security protocols with an unbounded number of sessions and unlimited fresh data for which the problem of secrecy is decidable. The only constraint placed on the class is a notion of depth-boundedness. @@ -16,4 +16,4 @@ CSF'17 is an annual conference for researchers in computer security, to examine the formal models that provide a context for those theories, and techniques for verifying security. Originally a workshop of the [IEEE Computer Society's Technical Committee on Security and Privacy](http://www.ieee-security.org/), the meeting became a “symposium†in 2007, with a number of important papers and techniques having been presented first at CSF. -This year's papers are now available on the [CSF'17 conference's website](http://csf2017.tecnico.ulisboa.pt/accepted.html) \ No newline at end of file +This year's papers are now available on the [CSF'17 conference's website](http://csf2017.tecnico.ulisboa.pt/accepted.html).