New research project DETIPS

Markus Roggenbach and John Tucker, in collaboration with their colleagues Mark Jones and Xianghia Xie from the Visual Computing Group were awarded an EPSRC grant for their research project Data Release – Trust, Identity, Privacy and Security (DETIPS).   



Wordpress is loading infos from ukri

Please wait for API server to collect data from

Data Release – Trust, Identity, Privacy and Security Mark Jones (PI), Markus Roggenbach, John Tucker and Xianghua Xie (CoIs) EPSRC grant The Open Data Initiative (ODI) demonstrates that there is a growing ambition from government to publish internal data as open data sets. (See Data custodians, particularly large governmental organisations such as the DVLA and HMRC, have a legal duty, enforced by the Information Commissioner’s Office (ICO), and social duty of care to the public, to ensure that privacy is not breached by the release of data as open data sets. These large organisations face an increasingly difficult task in establishing whether the release of data will result in enough data being open to triangulate individuals and destroy privacy. Our research takes a collaborative approach uniquely combining formal methods, counter-fraud, data mining and data visualization to produce new tools, methodologies and theory for working with data release. We will produce tools that allow interactive analysis of data sets to determine if data release can combine with existing data to triangulate personal data. We will take a new approach of using formal notions about data, memorandums of understanding (of data use) and criteria of control to auto-generate software tools that allow the user to manipulate, investigate and analyse data sets for potential unintended consequences if released. We will undertake empirical studies with data keepers, data users and members of the public to inform data policies surrounding release of data and integrate this within our toolsets and methodologies.


Nao Hirokawa visiting

Nao Hirokawa from the Japan Advanced Institute of Science and Technology (JAIST) is visiting Swansea from 15 to 17 March. Nao is an expert in Term rewriting theory. The abstract of his seminar talk about Basic Normalization on Thursday, 15 March can be found here.  

Achim Jung visiting

Achim Jung from the University of Birmingham is visiting Swansea on Wednesday, 20 January 2016. He will give a talk in the PCV seminar series. Title: On the sobriety of domains Abstract: There are two ways in which a domain (in the sense of Dana Scott) may arise from countable data: The classic way is via order-theoretic approximation inside the domain, and leads to the notion of algebraic and continuous domains. Alternatively, one can view a domain as arising from the lattice of predicates that may be formulated for a data type. This latter approach was pioneered and developed by Samson Abramsky in his Domain Theory in Logical Form. I will explain these two approaches and then present an example that illustrates some of the subtlety that we may observe with the latter. Time: 4-5 pm Venue: Robert Recorde Room (Faraday Building 205) The talk will be preceded by a talk by Margarita Korovina.    

ETWG-RC Meeting

On November 12th and 13th Markus Roggenbach, Xu Wang and Phillip James went to the 3rd meeting of the ETWG-RC in Amsterdam. The session was chaired by Markus and Swansea presented recent work towards modelling ERTMS in Real-Time Maude (presented at FTSCS 2015). Talks from other participants included: Jan Peleska (Bremen): Complete Bounded Model Checking and Testing of Interlocking Systems. Alessandro Fantechi (Firence): Certification challenges of innovative signalling systems.  Marielle Stoelinga (Twente): Railway Maintenance Engineering (in co-operation with ProRail) . Jan Pelseka (Bremen): Overview on OpenETCS. Jaco van de Pol (Twente) / Anne Haxthausen (Lyngby): Introduce/discussion about the Rascal working group on Verification Technology. A good time was had by all with many fruitful discussions and ideas being exchanged. The Swansea Railway Verification Group dearly missed Monika who heroically stayed in Swansea in order to help organise the yearly departmental colloquium to be held next week in Gregynog, but we thank her for all her hard work towards our presentation slides. Faron will also be doubly sorry for unfortunately having to miss the trip, not only for missing the Science but also the tasty meals and refreshing beverages!

PCV seminar series

The seminar series Proof, Complexity, Verification (PCV) is a forum for presenting new results and ongoing work in Computer Science. It focuses on logic related themes, in particular Proof Theory, Complexity Theory and Program Verification. The seminars comprises talks by external and internal speakers.


Theoretical Computer Science Swansea has one of the largest groups of theoretical computer scientists in the UK, with a research programme focused by these questions: Computability Dr Jens Blanck, Professor John Tucker What can and what cannot be computed, now or in the future? We are extending the classical theory of digital computation, expanding the conception of computation to deal with any form of discrete and continuous data, any physical form of data representation, and any physical means of computation. Read more about computability… Specification Professor Peter Mosses, Dr Markus Roggenbach What is a system supposed to do? The accurate and unambiguous specification of software and hardware systems is a massive problem. We pursue radical new approaches to the design and construction of programming and specification languages. Read more about specification… Proof theory Dr Ulrich Berger, Dr Monika Seisenberger, Dr Anton Setzer Does a system actually do what it is supposed to do? Reasoning about huge systems is necessary and difficult. Our work pushes the limits of proof, builds tools using constructive type theory and logics, and applies them to problems such as railway signalling systems. Read more about proof theory… Complexity Professor Arnold Beckmann, Dr Oliver Kullmann, Professor Faron Moller How hard is it to verify the correctness of programs? This question is intrigues researchers who want to measure the complexity of proofs, find the fastest SAT-solver, and improve model checking tools for systems. Read more about complexity… Railway Verification Professor Faron Moller, Dr Markus Roggenbach, Dr Monika Seisenberger, Dr Anton Setzer In 2007, we started a collaboration with Invensys Rail, a multinational technology leader based in Chippenham, which provides state-of-the-art signalling, communication and control systems for mainline and mass transit rail networks across the world. The success of this collaboration resulted in the creation of the Swansea Railway Verification Group. Research carried out by the group is having impact on both current practices and strategic planning within the railway industry. Read more about railway verification…  


Professor Arnold Beckmann Our HoD Dr. Ulrich Berger My traditional work areas are domain theory, proof-theory and lambda calculus. Currently, I’m mainly working on program extraction from proofs. Dr. Jens Blanck Dr. Xiuyi Fan Dr. Oliver Kullmann Dr. Liang-Ting Chen Dr. Phillip James Professor Faron Moller Dr. Liam O’Reilly Dr. Arno Pauly Professor Markus Roggenbach Dr. Monika Seisenberger Dr. Anton Setzer Professor John V. Tucker    Dr. Ferdinand Vesely    PhD students: Hoda Abbasizanjani Hoda is a PhD student in Theoretical Computer Science. Her current research is about the connections of SAT (the propositional satisfiability problem) and combinatorics. The main goal of her research is to study the structure of minimally unsatisfiable clause-sets (conjunctive normal forms as set-systems) in order to understand the reasons of unsatisfiability (inconsistency). Arved Friedemann Research area: Extracting advanced SMT solvers from proofs     Olga Petrovska The aim of my research is finding an efficient way of extracting programs from proofs. This is an alternative approach to software development, where correctness properties of software specifications are formally proved and software is extracted from this proof.

CCC 2015

The workshop “Continuity, Computability, Constructivity – From Logic to Algorithms” (CCC 2015)  was held in Schloss Aspenstein, Kochel am See, near Munich, 14-18 September 2015. This was the fourth and final workshop of the EU FP7 project ” COMPUTAL (Computable analysis – theoretical and applied aspects), a research network between Europe, Russia, South-Africa,and Japan. The event was organised by Monika Seisenberger and colleagues from Swansea. More information about the event including abstracts and links to previous CCC workshops can be found at