David Pym (Principal Investigator) 

csm_David_Pym_1_736cfa766aDavid is a logician, mathematician, and computer scientist. His research is mainly in logic, where he works in both pure logic and on developing logic-based methods as a mathematical modelling technology for reasoning about systems and behaviour, and in security, where he works in security policy, security economics, and systems security modelling.

His contributions have been mainly in the following areas: dependent type theory and logical frameworks, including proof theory, semantics, and unification algorithms; reductive logic and proof-search, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of reduction; the bunched logic BI and its relatives, including proof theory, semantics, algebraic theory, and computational interpretations, and their applications to program logics, including Separation Logic, and security; distributed systems modelling based on resource semantics and process algebra; modal and epistemic bunched logics and layered graph logics, with applications in access control; utility-theoretic concepts in distributed systems modelling and process algebra, with applications in systems security modelling; trust domains; information security economics; the philosophy and methodology of information security; public policy in information security, including information stewardship.

He has a broad experience of research, teaching, and management in leading universities and in industry.

George Danezis (Co-Investigator)

George DGeorge Danezis is a Professor of Security and Privacy Engineering at the Department of Computer Science of University College London, and Head of the Information Security Research Group. He has been working on anonymous communications, privacy enhancing technologies (PET), and traffic analysis since 2000. He has previously been a researcher for Microsoft Research, Cambridge; a visiting fellow at K.U.Leuven (Belgium); and a research associate at the University of Cambridge (UK), where he also completed his doctoral dissertation under the supervision of Prof. R.J. Anderson.

His theoretical contributions to the Privacy Technologies field include the established information theoretic and other probabilistic metrics for anonymity and pioneering the study of statistical attacks against anonymity systems. On the practical side he is one of the lead designers of the anonymous mail system Mixminion, as well as Minx, Sphinx, Drac and Hornet; he has worked on the traffic analysis of deployed protocols such as Tor.

His current research interests focus around secure communications, high-integirty systems to support privacy, smart grid privacy, peer-to-peer and social network security, as well as the application of machine learning techniques to security problems. He has published over 70 peer-reviewed scientific papers on these topics in international conferences and journals.

He was the co-program chair of ACM Computer and Communications Security Conference in 2011 and 2012, IFCA Financial Cryptography and Data Security in 2011, the Privacy Enhancing Technologies Workshop in 2005 and 2006. He sits on the PET Symposium board and ACM CCS Steering committee and he regularly serves in program committees of leading conferences in the field of privacy and security. He is a fellow of the British Computing Society since 2014.

Peter O’Hearn (Co-Investigator)

csm_Peter_O_Hearn_01_a50a3ef5acPeter is a Research Scientist working with the Static Analysis Tools team in the Facebook London Engineering office. I came to Facebook in 2013 with the acquisition of the verification startup Monoidics, and before that he held academic positions at Syracuse University, Queen Mary University of London and University College London. He maintains a part-time Professor position at UCL.

His research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of formal proof. With John Reynolds he developed separation logic, a theory which opened up new practical possibilities for program verification. Subsequent work in academic program analysis eventually led to the the Monoidics/Facebook Infer program analyzer, which is notable for supporting deep reasoning about big code that is undergoing rapid concurrent modification. Infer currently runs in production at Facebook, where it helps thousands of bugs be fixed each month before reaching production.

He has received a number of awards for his work in verification including the 2016 CAV Award and the 2016 Godel Prize. He was elected fellow of the UK Royal Academy of Engineering in 2016.

Edmund Robinson (Co-Investigator)

edmund-smallEdmund is a mathematician and computer scientist.  He was educated at Cambridge, obtaining my PhD in mathematics in 1984. He then took a research position at the Department of Computer Science in Edinburgh, before returning to Cambridge as a research fellow. In 1987 he left his fellowship for an Assistant Professorship at Queen’s University in Canada. From there he came back to the UK in 1990 as first a lecturer, then an EPSRC Advanced Fellow and finally a Reader at the School of Cognitive and Computing Sciences in Sussex. His last move was when he came to Queen Mary as Professor in 1995. In 2002 he was appointed Head of the Department of Computer Science and then charged with its merger with Electronic Engineering to form the new School of Electronic Engineering and Computer Science, of which he was the founding Head until August 2010. Since coming to the end of his term as Head he has been on sabbatical, and filling in for Prof Ursula Martin as Acting Director of ImpactQM. For more details check his CV.

James Brotherston (Co-Investigator)

James Brotherston is a Reader in Logic and Computation in the Dept. of Computing at UCL, where he is a member of the Programming Principles, Logic and Verification (PPLV) research group.  James holds a PhD from the School of Informatics, University of Edinburgh 2006; he was then a postdoctoral researcher at Imperial College London and, briefly, a lecturer at Queen Mary University of London before moving to UCL in 2012.

James’ main research interests lie in mathematical logic and its application to computer science, especially in automated program verification. He is especially well known for his pioneering work on cyclic proof, and for his work on the foundations of separation logic.

Byron Cook (Co-Investigator)

Byron's Bio PhotoByron Cook is Professor of Computer Science at University College London (UCL) and Director at Amazon Web Services. Byron’s interests include computer/network security, program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems. At Amazon Byron leads a research group focused on formal/constraint-based tools for reasoning about cloud-computing security.

William Venters (Co-Investigator)

Dr Will-Venters_724Will Venters is an Assistant Professor in Information Systems and Digital Innovation within the Department of Management at the London School of Economics and Political Science (LSE). His research interests include cloud computing, digital platforms and digital innovation approaches. He has a first-class degree in computer science and a PhD in information systems. His research work has been published in major refereed journals including MIS Quarterly, Journal of Information Technology, the Journal of Management Studies, and the Information Systems Journal. He co-authored the Palgrave book “Moving to the Cloud Corporation” and is the author of a blog on digital technology and is an associate editor of the Journal Information Technology and People. He speaks regularly at practitioner conferences on various digital business issues, particularly around Digital Ecosystems, Digital Innovation and Cloud Computing; has briefed  European government policy makers and various company executives; and has undertaken consultancy in IT strategy and Digital issues

Alastair Donaldson (Co-Investigator)


Alastair Donaldson is a Reader and EPSRC Early Career Fellow in the Department of Computing, Imperial College London, where he leads the Multicore Programming Group, and is director of GraphicsFuzz, a spin-out company specialising in automated testing for graphics drivers. He is the recipient of the 2017 BCS Roger Needham Award for his research into many-core programming. He has published more than 70 peer-reviewed papers on programming languages, formal verification, software testing and parallel programming, and leads the GPUVerify project on automatic verification of GPU kernels – a collaboration with Microsoft Research – and the GLFuzz project on automated testing for graphics shader compilers. Alastair coordinated the FP7 project CARP: Correct and Efficient Accelerator Programming, which completed successfully in 2015. Before joining Imperial, Alastair was a Visiting Researcher at Microsoft Research Redmond, an EPSRC Postdoctoral Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow, and is a Fellow of the British Computer Society

John Wickerson (Co-Investigator)

J WickersonJohn Wickerson is a Lecturer in the Department of Electrical and Electronic Engineering at Imperial College London. He has a PhD in Computer Science from the University of Cambridge. His research is on the application of formal methods to high-performance computing. Some topics he has published on include: the concurrency semantics of the OpenCL language; automatic compiler testing; testing implementations of transactional memory; and software-to-hardware compilation. He is a Senior Member of the IEEE.

Research Associates and Fellows

Roser Pujadas (Research Fellow)

Rosa PurjadasDr Roser Pujadas is a Research Fellow in Information Systems, undertaking research on the organisational, managerial and social implications of digital interfaces, as part of the EPSRC-funded project Interface Reasoning for Interacting Systems (IRIS). This is a relevant area of research as many digital innovations including the Internet of Things, Smart Cities, Platforms and Artificial Intelligence, involve a myriad of systems owned and operated by various companies which become tightly coupled through their interfaces (e.g. APIs and cloud computing); yet little is known about how the organisations involved in such innovations define such digital interfaces, how they evolve, and in particular what organisational or management commitments are embedded within them or how new forms of organisation or technology emerge through their use.

Diana Costa (Research Associate)

Diana CostaDiana Costa is a postdoctoral researcher at the Programming Principles, Logic and Verification Group at UCL. She was awarded her PhD in Applied Mathematics in 2019 from a joint program between the Universities of Aveiro, Porto and Minho. In her thesis Diana developed paraconsistent versions of hybrid logics capable of dealing with (what would be classically defined as) inconsistencies both at the level of propositional variables and the accessibility relations. Her project about the applications of this theme in the field of robotics earned her the 2015 Gulbenkian Prize for Stimulus to Scientific Research in the field of Mathematics. She has also worked with classical hybrid logics, focusing mainly on Herbrand-like theorems for hybrid logics and translations.
In the IRIS project Diana has been working on the development of separation-style logics to deal with graphs, under the point of view that they reflect the behavior of interfaces.
Her main interests go around the development of new logical systems built upon graphs, at the same time that she is still keen of paraconsistent reasoning and many-valued logics.

Paul Brunet (Research Associate)

Paul Brunet 3Paul Brunet has been a Research Associate in Programming Principles, Logic and Verification (PPLV) group at UCL’s Dept. of Computer Science since January 2017. In October 2016 Paul obtained a PhD from the University of Lyon, under the supervision of Damien Pous.

His research focuses on theoretical aspects of software verification. More specifically Paul studies the algebraic properties of various models of program behaviour. His interests also include logic, automata theory, mechanised proofs, concurrency theory and nominal mathematics. He has authored a dozen papers in peer-reviewed international conferences and journals on some of these topics.

Kang Feng (Research Associate)

Kent Feng

Kang Feng Ng is a Postdoctoral Research Assistant at the School of Electronic Engineering and Computer Science (EECS) of Queen Mary University of London (QMUL). Kang Feng obtained his PhD from the University of Oxford under the supervision of Prof Bob Coecke. He was a Postdoctoral Researcher at Radboud University before joining QMUL.

Kang Feng is interested in a wide array of applied category theory. He mainly worked on diagrammatic calculi, a visual presentation of (strict) monoidal categories, especially in quantum computing.

Alessio Santamaria (Research Associate)

FB profile pictureAlessio Santamaria studied Mathematics at the University of Genoa, where he obtained a Master’s Degree with a dissertation on Frames and Equilogical Spaces, supervised by Prof Pino Rosolini, in 2015. He then moved to Bath to undertake a PhD in Theoretical Computer Science with Prof Guy McCusker, which he passed in the summer of 2019. His thesis, “Towards a Godement Calculus of Dinatural Transformations”, solves the long-standing problem of compositionality of dinatural transformations, which are categorical structures used, in Computer Science, to capture Strachey’s idea of parametric polymorphism and to interpret proofs in intuitionistic and multiplicative linear logic. The original motivation which led Alessio into the studying of dinatural transformations was an attempt to give an algebraic understanding to Guglielmi and Gundersen’s “atomic flows”, a geometrical structure that can be extracted from logical proofs in Deep Inference.
Alessio’s research interests are in pure as well as applied Category Theory. Now a Postdoctoral Research Assistant at Queen Mary University of London, he is investigating categorical tools to apply within the IRIS project.

Matthew Windsor (Research Assistant)

WindsorMatt Windsor is a Research Associate at the Department of Computing, Imperial College London, and is finishing a PhD in Computer Science at the University of York.  His main area of interest is the correctness of concurrent programs; his thesis concerns the automatic verification of properties of concurrent programs using a separation-style program logic, and his focus as a research assistant is checking that C compilers compile concurrent code correctly according to the language standards.

Matt has also been an intern at Microsoft Research, Cambridge, where he helped prototype extensions of the C# programming language to support Haskell-style typeclasses.

Max Kanovich (Research Associate)


PhD Students

Rohit Nair (PhD Student)

rohit nair


University College London (UCL)

Imperial College London

London School of Economics (LSE)

Queen Mary, University of London (QMUL)

Industry Partners:

Amazon Web Services (UK) BT Facebook (International)
GridPP HP Labs Methods Group