People

Investigators

David Pym (Principal Investigator)

David 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 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)

Peter 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 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 Cook is Professor of Computer Science at University College London (UCL) and VP/Distinguished Scientist 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 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 www.binaryblurring.com 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)

John 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 Fellows

Roser Pujadas (Senior Research Fellow)

Dr 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.

Quang Loc Le (Research Fellow)

Quang Loc Le is a Research Fellow in the Programming Principles, Logic and Verification Group at UCL. He has a PhD in Computer Science from the School of Computing, National University of Singapore 2014. His research is on automated program verification and software testing.

Enrico Rossi (Research Fellow)

Enrico is a Research Fellow in the UCL Department of Computer Science, and part of the EPSRC-funded project Interface Reasoning for Interacting Systems (IRIS), where he focusses on the modelling and theorization of digital interfaces. For the past three years and until 2020, Enrico has served as an LSE Fellow at the Information Systems and Innovation Faculty Group of the Department of Management of the London School of Economics (LSE). Enrico has been awarded his PhD from the LSE on the governance and regulation of digital infrastructures

Enrico’s research mainly focuses on the law and economics of infrastructures and distributed systems, on the problems emerging from the digitization of property rights and contracts over digital networks, on the role played by digital interfaces in the governance of digital networks, and on the organizational and managerial implications of the transition from digital platforms to digital infrastructures. He is an expert in distributed systems and blockchain technology and co-created and currently leads the LSE online course on cryptoassets and blockchain.

Before that, Enrico obtained a Master degree in industrial engineering from the University of Bologna and worked as a management consultant for EY Rome.

Kang Feng (Research Fellow)

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 Fellow)

Alessio 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.

Max Kanovich (Research Associate)

Max has a PhD and a Dr.Hab in mathematics, physics, mathematical logic and computer science. He has a great experience of working in a research environment. He has a reknown expertise in CS and Math, including inductive and abduction theorem proving, separation logic and program analysis techniques. He has a strong background in verification, automated reasoning, program logics, etc., as evidenced by my work history and publication record (over 120 published refereed papers).

Estibaliz Fraca (Research Fellow)

Estibaliz Fraca is a Research Fellow in the Programming Principles, Logic and Verification (PPLV) group at UCL. She has a PhD in Computer Science from Universidad de Zaragoza. Her thesis contributes to the study of fluidization of Petri nets, a known formalism for the modelling and analysis of Discrete Event Systems. It was awarded as the “best thesis in modelling, simulation and optimization” by the Spanish Committee of Automatic Systems in 2015. Her research ranges from studying the theoretical complexity of Continuous Petri nets to modelling of distributed systems.
She has participated in a Knowledge Transfer Partnership on the design and evaluation of Educational Technology in UCL Knowledge Lab. She is interested in the modelling and analysis of how distributed systems interact. Her current research in IRIS focuses on formal verification of software, including Concurrent Separation Logic.

Vasilis Klimis (Research Fellow)

Vasilis Klimis is a postdoctoral researcher in the Department of Electrical and Electronic Engineering at Imperial College London. His current research focuses on building computational (machine, language and run-time) models with the larger goal of making the underlying system more reliable and performant; at the same time easier to design, understand, and manage. In the past he has worked on analysis of software-defined networks. He had twenty years of experience in the telecom industry before switching to academic research.

Timo Lang (Research Fellow)

Timo Lang joined the Programming Principles, Logic and Verification Group at UCL as a Postdoctoral Researcher in June 2021. He obtained a Master’s degree in mathematics and then pursued a PhD in computer science at the university of Vienna, which culminated in a thesis on the proof theory of substructural logics.

Timo is interested in the semantics and proof theory of various nonclassical logics as well as their implementation as a reasoning tool in computer science. His current research in IRIS focuses on the formal modelling of distributed systems.

Anushri Gupta (Research Fellow)

Dr Anushri Gupta is a Research Officer at the Information Systems Research Group, Department of Management at LSE. Her research interests include studying how advances in technology and data can be harnessed to create effective and collaborative forms of governance, and support data sharing in cities. This entails applying an interdisciplinary approach to research innovation and managerial issues in digital government, smart urban governance, and data ecosystems. Her work has been published and presented at major refereed academic journals and conferences. She has also written for the European Commission and participated in a discussion with the EU commissioner for cohesion policy. She also serves as an area editor for the Data & Policy journal and its associated conference Data for Policy on a specialised track on “Focus on the Policy Frameworks, Governance and Management of Data-driven Innovations”. Anushri holds a Masters in Electronic Engineering with Management from King’s College London and a PhD from Queen Mary University, London.

Jack Clark (Research Fellow)

Jack Clark joined the Multicore Programming Group at Imperial College London as a Research Associate in October 2021. He obtained a master’s degree in computer science from ETH Zurich that included a thesis proposing a novel method of verifying serializable concurrency control protocols in database systems. His interests include the automatic testing and verification of distributed systems as well as automatic fuzz testing of wider software systems.

PhD Students

Marius-Constantin Ilau (PhD Student)

Marius is a Research Student at the Department of Computer Science, UCL, London, pursuing a PhD in modelling organisational structures, infrastructures and security policies. His areas of interest include but are not limited to technical, managerial and psychological aspects of information security, systems optimisation and modelling in various organisational contexts. He previously studied Computer Science at the Alexandru Ioan Cuza University of Iasi, where he obtained a BSc Degree with a dissertation on Procedural Generation of Realistic 3D Terrain. Then, he moved to UCL to undertake an MSc in Information Security, which was finalised with a dissertation on the ability to use grammar inference algorithms to optimise the data structures used by traditional IDS systems with respect to storage space, to increase their viability in the actual IoT context. Furthermore, Marius was a security & privacy intern at Continental AG. His responsibilities included producing different analysis documents related to the ISO 26262 (technical risk analysis, failure mode effect analysis) and 27000 (attack tree analysis, security concept) standards while providing information security advice to teams involved in the production of functionalities related to the self-driving car.

Rohit Nair (PhD Student)

Previous Members

Matthew Windsor (Research Assistant)

Matt 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.

Diana Costa (Research Fellow)

Diana 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 Fellow)

Paul 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.