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.


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