Professor Samson Abramsky FRS was awarded an Honorary Doctorate by Middlesex University. Samson is the Christopher Strachey Professor of Computing at the Department of Computer Science at the University of Oxford. Samson has connections to the Foundations group. His PhD supervisor was Richard Bornat, and Samson was the PhD supervisor of Raja Nagarajan.
James Brotherston, Nikos Gorogiannis, Max Kanovich, and Reuben Rowe. Model checking for symbolic-heap separation logic with inductive predicates. POPL 2016.
Taolue Chen, Fu Song, and Zhilin Wu. Verifying Pushdown Multi-Agent Systems against Strategy Logics. IJCAI 2016.
Xincai Gu, Taolue Chen, and Zhilin Wu. A complete decision procedure for linearly compositional separation logic with data constraints. IJCAR 2016.
Guoxin Su, Taolue Chen, Yuan Feng, David S. Rosenblum, and P. S. Thiagarajan. An Iterative Decision-Making Scheme for Markov Decision Processes and Its Application to Self-Adaptive Systems. FASE 2016.
Manuel Bodirsky, Barnaby Martin, Michael Pinsker and András Pongrácz. Constraint satisfaction problems for reducts of homogeneous graphs. ICALP B 2016.
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi. CoSMed, a Confidentiality-Verified Social Media Platform. ITP 2016.
M. Bottone, G.Primiero, F. Raimondi, V. De Florio, A model for trustworthy orchestration in the Internet of Things. IE 2016.
Barnaby gave the Algorithms and Complexity Seminar at Durham on 30th November. His talk on “Minimal generating sets for direct powers of finite algebras” caused some consternation as it was largely disjoint from the fields of algorithms or complexity. One member of the group exclaimed that it was an hour of his life he’d never get back, to which Barnaby replied that this was how he felt whenever he heard a symphony of Shostakovich.
CoCon is a conference management system with confidentiality verified in the Isabelle theorem prover. It is being developed as a joint project between the Technical University of Munich and Middlesex. CoCon has just been successfully used for managing the paper submission and reviewing process at the TABLEAUX 2015 conference.
On Sept. 20, Andrei will give a half-day tutorial on inductive and coinductive datatypes at the TABLEAUX 2015 conference in Wroclaw.
Barnaby Martin has a paper accepted at CSL 2015, co-authored with Simone Bova, and titled “First-Order Queries on Finite Abelian Groups”. The 24th EACSL Annual Conference on Computer Science Logic will be held at the Technical University Berlin from Monday, 7 September 2015 to Thursday, 10 September 2015.
The paper Foundational Extensional Corecursion: A Proof Assistant Perspective by Andrei and his collaborators (Jasmin Blanchette and Dmitriy Tarytel) was accepted at ICFP 2015. It argues that total productive programming with lazy structures (also known as co-programming) is best hosted by a proof assistant, as opposed to an “ordinary” programming language.
Barny has been named the group’s Employee of the Month after his success at LICS and ICALP 2015.
Between the 2nd and the 9th of May, Giuseppe will be visiting the the Dept. of Computer and Systems Sciences at the Stockholm University and deliver 3 lectures for PhD students. The lectures will cover Computer Science as Abstraction and Control, Computational Correctness, and Software Theory Change.