- The EPSRC ‘Resource Reasoning’ platform research grant EP/H008373/2 ends.
- A project-wide meeting was held at UCL. See the meeting page for details of the speakers and slides.
- A project-wide meeting was held at UCL with representatives from the Advisory Panel and EPSRC in attendance. For full details, click here.
- This website has been migrated to GitHub pages, and is now being co-maintained with UCL. If you notice any incorrect information please feel free to report it on our project page.
- POPL 2013 takes place in Rome, with lots of participation from Resource Reasoning:
- Thomas Dinsdale-Young presents the paper “Views: Compositional Reasoning for Concurrent Programs”.
- Jules Villard presents the paper “The Ramifications of Sharing in Data Structures”.
- Peter O’Hearn gives a talk on “Program Logic and Analysis” at the co-located Programming Languages Mentoring Workshop.
- An informal Pre-POPL Yak, sponsored by Resource Reasoning, features talks by international experts on concurrency and verification.
- Resource Reasoning proudly sponsors the Programming Languages Mentoring Workshop, co-located in Rome with POPL on January the 22nd 2013. Students have until Sunday the 9th December to apply for funding to attend both PLMW and POPL for free!
- Dino Distefano presents the Needham Award lecture on 29th November for his work on program analysis with separation logic. Tickets are available here. The talk will be at the Royal Society in London. Check out the entertaining headline in the Italian press.
- Alexey Gotsman and Hongseok Yang’s paper “Linearizability with Ownership Transfer” receives the best paper award at CONCUR 2012.
- The Oxford Concurrency Workshop takes place on 9th and 10th July, continuing the series.
- Congratulations to Mark Wheelhouse for passing his PhD viva!
- James Brotherston moves to UCL as a Lecturer and EPSRC Career Acceleration Fellow
- Dino Distefano receives the BCS Roger Needham Award. The award is made annually for a distinguished research contribution in computer science by a UK-based researcher who has completed up to 10 years of post-doctoral research.
Peter O’Hearn and Byron Cook move to UCL, where they will start a new research group. Carsten Fuhs, Nikos Gorrogiannis and Jules Villard join them as postdocs, and Kaustubh Nimkar as a PhD student, all supported by the Resource Reasoning Programme grant.
Peter takes up a Royal Academy of Engineering/Microsoft Research Chair at UCL.
- POPL 2012 happens in Philadelphia, with lots of participation from Resource
Reasoning and friends:
- Philippa Gardner and Byron Cook give talks at the pre-POPL mentoring workshop.
- Tony Hoare receives the SIGPLAN Programming Languages Achievement Award. As part of the presentation, Peter O’Hearn interviews Hoare in front of the POPL audience.
- Hongseok Yang presents the paper “Abstractions from Tests” in the POPL main conference.
- Our mate Uday Reddy presents his joint paper with John Reynolds, “Syntactic Control of Interference for Separation Logic”, to rave reviews.
- Byron Cook and Peter O’Hearn give talks at the post-POPL TutorialFest.
- Yak goes international with a Pre-POPL Yak at New York University.
- Peter O’Hearn gives a joint invited lecture at APLAS/CPP 2011 in Taiwan, on a general theory of concurrency.
- Calcagno, Distefano, O’Hearn and Yang publish a 73-page paper on abductive program analysis in JACM, the leading journal in computing.
- Yak at Cambridge University on 9th December.
- Philippa Gardner delivers a keynote at FOOL’11 in Portland, on reasoning about a concurrent B-Tree algorithm.
- Peter O’Hearn delivers a keynote at ICFEM in Durham, on abductive program proving.
- Philippa Gardner delivers a keynote at CALCO 2011 in Winchester, on reasoning about a concurrent B-Tree algorithm.
- Peter O’Hearn gives a course at the Marktoberdorf PhD summer school.
- Byron Cook is an invited speaker at CADE 23 in Poland.
- Yak at Imperial on 29th July with special guest Bart Jacobs (Katholieke Universiteit Leuven).
- Congratulations to Thomas Dinsdale-Young for passing his PhD thesis defense on Abstract Data and Local Reasoning.
- Byron Cook gives a course at the ECOOP’11 PhD summer school.
- John Reynolds delivers the BCS Lovelace Lecture on 8th June on “Making Program Logics Intelligible”.
Byron Cook publishes a review article with his colleagues Podelski and Rybalchenko in CACM. It explains their seminal ideas on “Proving Program Termination” in a manner appropriate to the broad CACM audience.
Moshe Vardi comments on this work in his piece “Solving the Unsolvable” from the July ‘11 issue of CACM.
- The Dublin Concurrency Workshop takes place on 14th-15th April, continuing the series.
- Alexey Gotsman is awarded the EAPLS Best PhD Dissertation Award 2010 for his dissertation on “Logics and analyses for concurrent heap-manipulating programs”.
- Congratulations to Gareth Smith for passing his PhD viva.
- Hongseok Yang, Alexey Gotsman and Matthew Parkinson teach the course “Separation Logics and Applications” at the ENS Lyon Winter School in Computer Science.
- POPL 2011 takes place.
Samin Ishtiaq and Peter O’Hearn win the Most Influential POPL Paper Award for their POPL 2001 paper BI as an Assertion Language for Mutable Data Structures.
The award is presented annually to the authors of a paper presented at the POPL held 10 years prior to the award year. The papers are judged by their influence over the past decade.
- Web/concurrency yak at Imperial.
- John Reynolds gives the first Peter Landin Annual Semantics Seminar at the British Computer Society offices in London.
- Jeremy Dawson of ANU Canberra arrives to visit Imperial for ~1 month. He will be working with James Brotherston on interpolation for displayable logics.
- Peter O’Hearn talks on Reasoning about Programs Using a Scientific Method on 16th November in a BCS-FACS Evening Seminar at the London Mathematical Society.
- Mohammad Raza moves to Microsoft Research Cambridge.
- Geek of the Week interviews Byron Cook.
- Automation yak at Queen Mary . informal talks and demonstrations on automated verification including Xavier Rival (INRIA Roquencourt).
- Jules Villard arrives to start a postdoc at Queen Mary.
- Mohammad Raza passes his PhD with flying colours.
Abstraction yak at Imperial . informal talks, including Lars Birkedal (ITU Copenhagen) on Step-Indexed Kripke Models over Recursive Worlds.
- Dagstuhl Seminar on Modelling, Controlling and Reasoning About State takes place, organised by Ahmed, Benton, Birkedal and Hofmannm, with talks by Yang, Rinetzky and Gardner.
O’Hearn is a keynote speaker on Abductive, Deductive and Inductive Reasoning about Resources at CSL 2010.
Verified Software: Theories, Tools and Experiments 2010 takes place in Edinbugh, with O’Hearn a program chair, Yang a theory workshop chair, and Parkinson keynote speaker on The Next 700 Separation Logics. The conference was partly sponsored by EPSRC programme grant Resource Reasoning.
Sergio Maffeis awarded a five-year EPSRC Career Acceleration Fellowship at Imperial.
- Refinement mini-yak at Imperial . informal talks, including Aaron Turon (Northeastern University, visiting Microsoft) on A Separation Logic for Refining Concurrent Objects.
- Oukseh Lee arrives at Queen Mary for one year on Resource Reasoning project. He will be working with Hongseok Yang on automatic verification of operating systems programs.
- The Proof Systems for Program Logics workshop takes place at FLOC in Edinburgh, partly sponsored by EPSRC programme grant Resource Reasoning.
- John Reynolds arrives to visit Queen Mary and Imperial for six months.
- Steve Brookes arrives to visit Queen Mary for two months.
- John Reynolds wins the 2010 BCS Lovelace Medal.
- Noam Rinetzky awarded a 5-year Royal Academy of Engineering research fellowship at Queen Mary.
- Yak session at Imperial on 4th March.
- Nikos Gorogiannis hired as RA at Queen Mary on Resource Reasoning project.