diff --git a/README.md b/README.md index 03cf81f5725a566c061c02b01d56197a777a1eb2..b3ce80d51988f65ef8dd183254eec0194e6a5ec6 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,9 @@ --- layout: page -title: PSVG Group Website Readme +title: VTSS Group Website Readme --- -This readme file is published in its fully rendered form [on the website](https://vtss.doc.ic.ac.uk/README.html). +This readme file is published in its fully rendered form [on the website]({{site.baseurl}}{% link README.md %}). The source code for [this site](https://vtss.doc.ic.ac.uk) is [hosted on the DoC GitLab server](https://gitlab.doc.ic.ac.uk/resource-reasoning/vtss.doc.ic.ac.uk), you should have access to edit it if a member of the resource-reasoning group. diff --git a/_people/da-rocha-pinto.md b/_people/da-rocha-pinto.md index 97e081e06d35a81fff8b5dfa83327123b028050c..4510f800bf4391eadfe2cfc10b460a8c339bd986 100644 --- a/_people/da-rocha-pinto.md +++ b/_people/da-rocha-pinto.md @@ -9,5 +9,5 @@ alumnus: true --- Pedro was a PhD student and a Post Doc in the group, working on developing logics for verification of fine-grained concurrent programs. -Pedro defended his PhD thesis, [Reasoning with Time and Data Abstractions](https://vtss.doc.ic.ac.uk/publications/daRochaPinto2017Reasoning.html) in January 2017. +Pedro defended his PhD thesis, [Reasoning with Time and Data Abstractions]({{site.baseurl}}{% link publications/daRochaPinto2017Reasoning.html %}) in January 2017. He is currently working for [Collage.com, Inc.](https://www.collage.com/) a Michigan-based photo products e-commerce company. diff --git a/_people/naudziuniene.md b/_people/naudziuniene.md index dbe58459cf23eef1e27583608a3c13b7d1df9acf..9004c5754f06119136972543284c9b5c0cf795ed 100644 --- a/_people/naudziuniene.md +++ b/_people/naudziuniene.md @@ -6,7 +6,7 @@ webpage: http://www.doc.ic.ac.uk/~dn911/ email: d.naudziuniene11@imperial.ac.uk alumnus: true --- -Daiva defended her Ph.D. on [An Infrastructure for Tractable Verification of JavaScript Programs](https://vtss.doc.ic.ac.uk/publications/Naudziuniene2018Infrastructure.html) in March 2018. +Daiva defended her Ph.D. on [An Infrastructure for Tractable Verification of JavaScript Programs]({{site.baseurl}}{% link publications/Naudziuniene2018Infrastructure.html %}) in March 2018. From 2017 Daviva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn. diff --git a/_people/ntzik.md b/_people/ntzik.md index 6ae520ac01102f3deb7c25118ce9c07a245ba006..b00accca27c0b6176e9c8b9d5acf2c1056d749a9 100644 --- a/_people/ntzik.md +++ b/_people/ntzik.md @@ -11,7 +11,7 @@ alumnus: true Gian Ntzik, Phd student and Post Doc with the group. -Gian defended his thesis [Reasoning about POSIX File Systems](https://vtss.doc.ic.ac.uk/publications/Ntzik2017Reasoning.html) +Gian defended his thesis [Reasoning about POSIX File Systems]({{site.baseurl}}{% link publications/Ntzik2017Reasoning.html %}) in February 2017 and is currently working for [Amadeus](http://www.amadeus.com/web/amadeus/en_GB-GB/Amadeus-Home/About-us/Our-company/1319477448520-Page-AMAD_DetailPpal) in systems development and research. diff --git a/_people/raad.md b/_people/raad.md index d62df55c86a55b3f3750b8362c56192b32b799fd..21111600523807c36e632e23dedb5e3fd83a2c33 100644 --- a/_people/raad.md +++ b/_people/raad.md @@ -8,7 +8,7 @@ alumnus: true --- Azalea Raad was a PhD student with the group, defending her thesis -on [Abstraction, Refinement and Concurrent Reasoning](https://vtss.doc.ic.ac.uk/publications/Raad2017Abstraction.html) in February 2017. +on [Abstraction, Refinement and Concurrent Reasoning]({{site.baseurl}}{% link publications/Raad2017Abstraction.html %}) in February 2017. She is now a postdoctoral researcher at the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/), working with [Derek Dreyer](https://people.mpi-sws.org/~dreyer/) and [Viktor Vafeiadis](https://people.mpi-sws.org/~viktor/) and a member of the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/). diff --git a/_posts/2016-11-14-inferlab.md b/_posts/2016-11-14-inferlab.md index 01ca6fab6caa064a4f3469e0c8217f5ee3f12dfa..42a8ed976a56fc9ff5070fa24ba56556dd857a6a 100644 --- a/_posts/2016-11-14-inferlab.md +++ b/_posts/2016-11-14-inferlab.md @@ -2,7 +2,7 @@ title: Infer Lab at Imperial --- -The [Separation Logic](https://vtss.doc.ic.ac.uk/teaching/separationlogic.html) course team ran a lab on [Infer](http://fbinfer.com/), +The [Separation Logic]({{site.baseurl}}{% link teaching/separationlogic.md %}) course team ran a lab on [Infer](http://fbinfer.com/), an automatic verification tool based on separation logic, developed at [Facebook](https://www.facebook.com/inferstaticanalyzer/) where it is used every day to verify millions of lines of code. @@ -19,4 +19,4 @@ During the tutorial, one of the students, Lorenzo Paoliani, ran Infer on Connect and found several null dereference bugs. He reported this on github and submitted a pull request for fixing that problem, which has been accepted and now merged. -For more details and slides, see the [Infer Lab 2016](https://vtss.doc.ic.ac.uk/teaching/InferLab.html) page. \ No newline at end of file +For more details and slides, see the [Infer Lab 2016]({{site.baseurl}}{% link teaching/InferLab.md %}) page. \ No newline at end of file diff --git a/_posts/2016-12-15-Dolby.md b/_posts/2016-12-15-Dolby.md index d75cd5615a817b1795c44e30195e432924062235..e552e66de142509859811d1c7458bc973e2f53eb 100644 --- a/_posts/2016-12-15-Dolby.md +++ b/_posts/2016-12-15-Dolby.md @@ -3,11 +3,11 @@ 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. +in New York visited the VTSS 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://vtss.doc.ic.ac.uk/research/javascript.html) +in a [symbolic analysis for JavaScript]({{site.baseurl}}{% link research/javascript.md %}) 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 diff --git a/_posts/2017-01-13-Pedro_viva.md b/_posts/2017-01-13-Pedro_viva.md index d1f2036da1337e89de8c3ec93df2d7e306574e15..696bc61e649471c4fdc393b821e30c3b1eb3bceb 100644 --- a/_posts/2017-01-13-Pedro_viva.md +++ b/_posts/2017-01-13-Pedro_viva.md @@ -10,6 +10,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://vtss.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.html) for verifying concurrent programs with much better support for abstraction. +called [TaDA]({{site.baseurl}}{% link 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://vtss.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html). +Pedro's latest paper, accepted to ESOP 2017 is on [our publications page]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}). diff --git a/_posts/2017-02-01-Gian_viva.md b/_posts/2017-02-01-Gian_viva.md index 6fe6de06a929f715cf17c88c98872eb8ee9010fa..fc0399486583700d04d308084c73998b099df43a 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://vtss.doc.ic.ac.uk/people/ntzik.html). +More details on Gian’s research can be found [here]({{site.baseurl}}{% link _people/ntzik.md %}). diff --git a/_posts/2017-02-06-ESOP.md b/_posts/2017-02-06-ESOP.md index bb0589c4cbbf1186557c7f4fcc532142c21529a5..629d77b350d1db487a6514caaa9283e9e05972a5 100644 --- a/_posts/2017-02-06-ESOP.md +++ b/_posts/2017-02-06-ESOP.md @@ -3,17 +3,17 @@ title: Papers accepted at ESOP 2017 --- Two papers from the concurrency project team have been accepted at 26th European Symposium on Programming [(ESOP 2017)](http://www.etaps.org/index.php/2017/esop), -which will take place this April in Uppsala, Sweden. The first paper, [Abstract Specifications for Concurrent Maps](https://vtss.doc.ic.ac.uk/publications/Xiong2017Abstract.html), present the importance of abstract atomicity for reasoning fine-grained concurrent modules. -The second paper, [Caper: Automatic Verification for Fine-grained Concurrency](https://vtss.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html), presents a prototype tool for automated reasoning about concurrent modules. +which will take place this April in Uppsala, Sweden. The first paper, [Abstract Specifications for Concurrent Maps]({{site.baseurl}}{% link publications/Xiong2017Abstract.html %}), present the importance of abstract atomicity for reasoning fine-grained concurrent modules. +The second paper, [Caper: Automatic Verification for Fine-grained Concurrency]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}), presents a prototype tool for automated reasoning about concurrent modules. -The first paper, submitted by [Shale Xiong](https://vtss.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto](https://vtss.doc.ic.ac.uk/people/da-rocha-pinto.html), -[Gian Ntzik](https://vtss.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner](https://vtss.doc.ic.ac.uk/people/gardner.html), -[Abstract Specifications for Concurrent Maps](https://vtss.doc.ic.ac.uk/publications/Xiong2017Abstract.html) demonstrates that abstract atomicity +The first paper, submitted by [Shale Xiong](https://vtss.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}), +[Gian Ntzik](https://vtss.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}), +[Abstract Specifications for Concurrent Maps]({{site.baseurl}}{% link publications/Xiong2017Abstract.html %}) demonstrates that abstract atomicity is key to give a specification for concurrent map that allows better client reasoning. This paper also provides the first functional correctness proof of ConcurrentSkiplistMap in java.util.concurrent with respect to the abstract specification. The second paper accepted, submitted by Pedro Da Rocha Pinto, in collaboration with [Thomas Dinsdale-Young](http://cs.au.dk/~tyoung/), [Kristoffer Just Andersen](http://pure.au.dk/portal/en/persons/id(5e842a19-8b76-487a-8082-06b6d6ff2545).html) -and [Lars Birkedal](http://www.cs.au.dk/~birke/) from Aarhus University is [Caper: Automatic Verification for Fine-grained Concurrency](https://vtss.doc.ic.ac.uk/publications/Dinsdale-Young2017Caper.html). +and [Lars Birkedal](http://www.cs.au.dk/~birke/) from Aarhus University is [Caper: Automatic Verification for Fine-grained Concurrency]({{site.baseurl}}{% link publications/Dinsdale-Young2017Caper.html %}). The paper presents [Caper](https://github.com/caper-tool/caper), a prototype tool for automated reasoning about concurrent modules. Caper is based on symbolic execution, integrating reasoning about interference on shared resources. This enables Caper to verify the functional correctness of fine-grained concurrent modules. diff --git a/_posts/2017-06-16-Algebraic.md b/_posts/2017-06-16-Algebraic.md index 8a48f471ca6a435847739275879c97830fcb0fb0..a94d50d91de9fa754f9de9795c1b1b93f60c370e 100644 --- a/_posts/2017-06-16-Algebraic.md +++ b/_posts/2017-06-16-Algebraic.md @@ -4,7 +4,7 @@ title: Paper accepted at Concur 2017 Andrea Cerone has had a paper accepted at this year’s [International Conference on Concurrency Theory, (Concur 2017)](https://www.concur2017.tu-berlin.de/) which will be held in Berlin, Germany in September. -The paper, entitled [Algebraic Laws for Weak Consistency](https://vtss.doc.ic.ac.uk/publications/Cerone2017Algebraic.html) was written in collaboration +The paper, entitled [Algebraic Laws for Weak Consistency]({{site.baseurl}}{% link publications/Cerone2017Algebraic.html %}) was written in collaboration with [Alexey Gotsman]( http://software.imdea.org/~gotsman), IMDEA Software Institute, Madrid and [Hongseok Yang](http://www.cs.ox.ac.uk/people/hongseok.yang/Public/Home.html), University of Oxford, UK. The purpose of the CONCUR conferences is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications. The topics covered are Theory, Formal Modelling, Verification, Performance Evaluation and Engineering of concurrent, timed, and other systems. diff --git a/_posts/2017-08-12-cade.md b/_posts/2017-08-12-cade.md index 857ad804090c8bb353304918c6b5034348f41493..31b6b362c9645f518d4f246d3cabb08d8d47d9ba 100644 --- a/_posts/2017-08-12-cade.md +++ b/_posts/2017-08-12-cade.md @@ -5,7 +5,7 @@ title: Invited paper at the 26th International Conference on Automated Reasoning Philippa Gardner was one of the invited speakers at the this year’s [CADE conference](http://www.cade-26.info/), held in Gothenburg, Sweden, on 6-11 August 2017. Philippa presented an invited paper, [‘Towards Logic-based Verification of JavaScript Programs’](https://link.springer.com/chapter/10.1007/978-3-319-63046-5_2), -jointly written with [José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/) +jointly written with [José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/) and [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/) This position paper proposes a possible pathway to achieve scalable symbolic verification of JavaScript based on separation logic. diff --git a/_posts/2017-09-26-popl.md b/_posts/2017-09-26-popl.md index faf6005fdc8aea4fc4d60135b47d1fc1a04dcd84..d7c0432c102840be0b0724dbac46fad4c983e777 100644 --- a/_posts/2017-09-26-popl.md +++ b/_posts/2017-09-26-popl.md @@ -1,7 +1,7 @@ --- title: Paper accepted at POPL 2018 --- -[José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html), [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), +[José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}), [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/) and [Thomas Wood](https://www.doc.ic.ac.uk/~tw1509/), have had a paper accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages [(POPL 2018)](https://popl18.sigplan.org/). diff --git a/_posts/2017-10-02-gabriela.md b/_posts/2017-10-02-gabriela.md index 85d71c5bd78a17461098c01d0f824d3f48ddfd91..9e3c7b563e0b804f5f692f08f320c591eaf5ec12 100644 --- a/_posts/2017-10-02-gabriela.md +++ b/_posts/2017-10-02-gabriela.md @@ -4,7 +4,7 @@ title: Welcome to Gabriela Sampaio, new PhD student with the group --- -We are really happy to welcome [Gabriela Sampaio](https://vtss.doc.ic.ac.uk/people/sampaio.html), who has joined the group as a PhD student. +We are really happy to welcome [Gabriela Sampaio]({{site.baseurl}}{% link _people/sampaio.md %}), who has joined the group as a PhD student. Gabriela completed her BSc at the Federal University of Pernambuco (UFPE, Brazil) and as an undergraduate, she spent a year at the University of Kent, working on [Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html), diff --git a/_posts/2018-01-06-PhD_opportunity.md b/_posts/2018-01-06-PhD_opportunity.md index 1a3cf98fdb30f023660a849c74250c0ca377005f..1d963f340fa490139dde3fc56e18a1479e6039f6 100644 --- a/_posts/2018-01-06-PhD_opportunity.md +++ b/_posts/2018-01-06-PhD_opportunity.md @@ -3,7 +3,7 @@ title: PhD position, start date in October 2018 --- Philippa Gardner is currently looking for a PhD student, start date in October 2018, -to join the [Verified Trustworthy Software Specification Group](https://vtss.doc.ic.ac.uk/), +to join the [Verified Trustworthy Software Specification Group]({{site.baseurl}}), For more details, please see the note below from Philippa: diff --git a/_posts/2018-01-12-popl.md b/_posts/2018-01-12-popl.md index d278ce396875c4cdb7e4c0433c5deaea2e5db8c9..57844252e4c1f98f7e04c73c6ee3f9f587aef1ee 100644 --- a/_posts/2018-01-12-popl.md +++ b/_posts/2018-01-12-popl.md @@ -2,8 +2,8 @@ title: Paper presented at POPL18 --- -[José Fragoso Santos](https://vtss.doc.ic.ac.uk/people/fragoso-santos.html) presented his paper -[JaVerT: JavaScript Verification using Separation Logic](https://vtss.doc.ic.ac.uk/publications/FragosoSantos2018JaVerT.html), jointly authored +[José Fragoso Santos]({{site.baseurl}}{% link _people/fragoso-santos.md %}) presented his paper +[JaVerT: JavaScript Verification using Separation Logic]({{site.baseurl}}{% link publications/FragosoSantos2018JaVerT.html %}), jointly authored with [Petar Maksimović](https://sites.google.com/site/petarmaksimovic1981/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/), [Thomas Wood](https://www.doc.ic.ac.uk/~tw1509/) and [Philippa Gardner](https://www.doc.ic.ac.uk/~pg/), at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages [(POPL 2018)](https://popl18.sigplan.org/). diff --git a/_posts/2018-04-18-papers-accepted-april-18.md b/_posts/2018-04-18-papers-accepted-april-18.md index add94751055f100ef3a9115ac64e9e430867767f..072bcb902c8ceea1a6cb3c0721821f1df0de7612 100644 --- a/_posts/2018-04-18-papers-accepted-april-18.md +++ b/_posts/2018-04-18-papers-accepted-april-18.md @@ -7,8 +7,8 @@ publised. A second paper, also collaborative work with current and former resear has also just been accepted to ECOOP 18. The first paper, [A perspective on specifying and verifying concurrent modules](https://www.sciencedirect.com/science/article/pii/S2352220817300871) -by [Thomas Dinsdale-Young](https://cs.au.dk/~tyoung/), [Pedro da Rocha Pinto](https://vtss.doc.ic.ac.uk/people/da-rocha-pinto.html) -and [Philippa Gardner](https://vtss.doc.ic.ac.uk/people/gardner.html) has been published in the [Journal of Logical and Algebraic Methods in Programming](https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming). +by [Thomas Dinsdale-Young](https://cs.au.dk/~tyoung/), [Pedro da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}) +and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}) has been published in the [Journal of Logical and Algebraic Methods in Programming](https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming). In the paper, the authors survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. @@ -18,10 +18,10 @@ these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example. -The second paper, co-authored by [Gian Ntzik](https://vtss.doc.ic.ac.uk/people/ntzik.html), -[Pedro da Rocha Pinto](https://vtss.doc.ic.ac.uk/people/da-rocha-pinto.html), -[Julian Sutherland](https://vtss.doc.ic.ac.uk/people/sutherland.html) -and [Philippa Gardner](https://vtss.doc.ic.ac.uk/people/gardner.html) has just been accepted to the 32nd European Conference on Object-Oriented Programming +The second paper, co-authored by [Gian Ntzik]({{site.baseurl}}{% link _people/ntzik.md %}), +[Pedro da Rocha Pinto]({{site.baseurl}}{% link _people/da-rocha-pinto.md %}), +[Julian Sutherland]({{site.baseurl}}{% link _people/sutherland.md %}) +and [Philippa Gardner]({{site.baseurl}}{% link _people/gardner.md %}) has just been accepted to the 32nd European Conference on Object-Oriented Programming [(ECOOP 2018)](https://conf.researchr.org/home/ecoop-2018), which will be held in Amsterdam in July. In the paper, entitled A Concurrent Specification of POSIX File Systems, diff --git a/teaching/InferLab.md b/teaching/InferLab.md index 852a32567fd914e48f6cee8a0e71ad905267a3e1..e48d1b0815d9f89bf2849a7d3b0547eea1b98ae3 100644 --- a/teaching/InferLab.md +++ b/teaching/InferLab.md @@ -7,11 +7,11 @@ menu_order: 5 sub_menu_order: 2 --- -The [Separation Logic](https://vtss.doc.ic.ac.uk/teaching/separationlogic.html) course is a 4th-year MEng and MSc course +The [Separation Logic]({{site.baseurl}}{% link teaching/separationlogic.md %}) course is a 4th-year MEng and MSc course on local reasoning about programs that manipulate the heap at the [Department of Computing](http://www.imperial.ac.uk/computing), [Imperial College London](http://www.imperial.ac.uk). The course is led by [Philippa Gardner](/people/gardner.html), with support from [Jose Fragoso](https://www.doc.ic.ac.uk/~jfaustin/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/), -[Azalea Raad](http://www.soundandcomplete.org/) and [Julian Sutherland](https://vtss.doc.ic.ac.uk/people/sutherland.html). +[Azalea Raad](http://www.soundandcomplete.org/) and [Julian Sutherland]({{site.baseurl}}{% link _people/sutherland.md %}). As part of the course, [Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/) and [Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/) from Facebook came to Imperial College to talk about [Infer](http://fbinfer.com/), diff --git a/teaching/separationlogic.md b/teaching/separationlogic.md index cff7f4dae6fa59ca99f70c2eb5b11d2b58f7cabe..f1373c17e50090ee6921513f8184d3df1edbccdf 100644 --- a/teaching/separationlogic.md +++ b/teaching/separationlogic.md @@ -31,7 +31,7 @@ You will learn how to write program specifications and prove properties of progr You will learn about Smallfoot, a semi-automatic verification tool based on symbolic execution, and [Infer](http://fbinfer.com/), an automatic tool based on bi-abduction. This work constitutes a breakthrough, in that it is now possible prove properties about millions of lines of code, thus making the reasoning viable for industry. - As part of the course, Facebook with Imperial ran a lab on Infer. See our [Infer lab 2016 page](https://vtss.doc.ic.ac.uk/teaching/InferLab.html) for details + As part of the course, Facebook with Imperial ran a lab on Infer. See our [Infer lab 2016 page]({{site.baseurl}}{% link teaching/InferLab.md %}) for details * The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.