Resource Reasoning

January 2016 Research Meeting

Resource Reasoning project meeting, Wednesday, 13th January 2016, 10:00-17:00. 6.12 Malet Place Engineering, UCL, Gower Street, WC1E 6BT

Attendees

TBC

Schedule

| Time | Speaker | Title | Affiliation | | —- | ——- | —– | ———– | | 09:45 – 10:00 | Tea, Coffee and Biscuits | | 10:00 – 10:15 | David Pym | Introduction | UCL | | 10:15 – 10:45 | Peter O’Hearn | | UCL/Facebook | | 10:45 – 11:15 | Daiva Naudziuniene | A Principled Intermediate Language for JavaScript Verification | Imperial | | 11:15 – 11:45 | Ilya Sergey | Hoare-style Specifications as Correctness Conditions for Non-Linearizable Concurrent Objects | UCL | | 11:45 – 12:15 | Matthew Parkinson | Starling: Automating Concurrency Verification | MSR | | 12:15 – 13:00 | Lunch | | 13:00 – 13:30 | Fredrik Dahlqvist | Positive Modal Separation Logics | UCL | | 13:30 – 14:00 | Philippa Gardner | Modern Concurrent Separation Logics | Imperial | | 14:00 – 14:30 | Jonathan Spring | Deciding the model’s features for a logic of information | UCL | | 14:30 – 15:00 | Gabrielle Anderson | Substructural Modal Logic for Optimality and Games | UCL | | 15:00 – 15:30 | Gian Ntzik | Fault-Tolerant Resource Reasoning | Imperial | | 15:30 – 16:00 | Reuben Rowe | Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates | UCL | | 16:00 – 16:30 | Cliff Jones | | Newcastle | | 16:30 – 17:00 | Impromptu Talks |