The following is a list of researchers from Microsoft Research and the IMDEA Software Institute that are collaborating in the context of the Joint Research Center. For more information please visit their home pages or the section on research topics.
Aditya Nori (Home Page at Microsoft Research India)
I am a member of the PLATO and MLO areas at Microsoft Research India. I am also an adjunct professor at IIT Hyderabad. My research interests include algorithms for the analysis of programs and machine learning with special focus on tools for improving software reliability and programmer productivity. I obtained my PhD from the Indian Institute of Science, Bangalore and Priti Shankar was my advisor.
My research interest is in the design and implementation of programming languages and methodologies that facilitate specification and verification of various program properties. My recent focus has been on the design of a programming language which integrates the well-known program logics, like Hoare and Separation Logic, with modern programming features for abstraction, information hiding and code reuse, such as higher-order functions, monads, polymorphism and modules.Alexey Gotsman (Home Page at IMDEA Software Institute)
I am a tenure-track Assistant Research Professor at the IMDEA Software Institute. Before joining IMDEA, I was a postdoctoral fellow at the University of Cambridge, where I also got my Ph.D. My research interests are in software verification, particularly, in developing reasoning techniques and automated verification tools for real-world concurrent systems software.
I am a Principal Researcher at Microsoft Research, Cambridge, where I manage Programming Principles and Tools. As a part-time position, I also hold the Chair in Computer Security and am a member of the Laboratory for Foundations of Computer Science and the Security and Privacy group in the School of Informatics in the University of Edinburgh. I convene the University of Edinburgh Microsoft Research Joint Initiative in Informatics. I participate in the Data Science PhD programme..Andrey Rybalchenko (Home Page at Microsoft Research)
Computer scientist Andrey Rybalchenko has developed a new method for finding software bugs. Traditional automated testing systems detect when programs do “bad things” that lead to crashes, forcing the program to quit. In a collaboration with Microsoft that began in 2006, Rybalchenko incorporated his methods into Terminator, a commercial program used to find bugs in the device drivers that mediate between an operating system and various pieces of hardware.
Anindya Banerjee received his PhD from Kansas State University, USA, in 1995. After his PhD, Anindya was a postdoctoral researcher, first in the Labaratoire d’Informatique (LIX) of Ecole Polytechnique, Paris and subsequently at the University of Aarhus. He joined the IMDEA Software Institute in February 2009 as Full Professor. Immediately prior to this position, Anindya was Full Professor of Computing and Information Sciences at Kansas State University, USA. He was an Academic Visitor in the Advanced Programming Tools group, IBM T. J. Watson Research Center in 2007 and a Visiting Researcher in the Programming Languages and Methodology group at Microsoft Research in 2007–2008. He was a recipient of the Career Award of the US National Science Foundation in 2001.
Ben Livshits (Home Page at Microsoft Research Redmond)
Ben Livshits is a research scientist at Microsoft Research and an affiliate professor at the University of Washington. Originally from St. Petersburg, Russia, he received a bachelor’s degree in Computer Science and Math from Cornell University in 1999, and his M.S. and Ph.D. in Computer Science from Stanford University in 2002 and 2006, respectively. Dr. Livshits’ research interests include application of sophisticated static and dynamic analysis techniques to finding errors in programs.
I joined the IMDEA Software Institute after completing my Ph.D. in the Information Security group of ETH Zurich and working as a postdoc in the Information Security and Cryptography Group of the Max Planck Institute for Software Systems. Before that, I studied mathematics at the Universidad de Chile, the Universidade Federal de Campinas, and the University of Konstanz, from which I received a M.Sc.
I am interested in security, programming, and distributed systems. I am a member of the Programming Principles and Tools and Security groups at Microsoft Research in Cambridge, UK. Since 2006, I also lead a project on Secure Distributed Computations at the MSR-INRIA Joint Center in Orsay, France. My recent research subjects include models for cryptography, information-flow security, secure multiparty sessions, refinement types for F#, authorization policies, secure logs, secure implementations of communication abstractions, access control for mobile code, concurrency in C#, private authentication, and the verification of cryptographic protocols for Internet security and Web Services security.Cesar Kunz (Home Page at IMDEA Software Institute)
César Kunz received a Computer Science degree from the National University of Córdoba (UNC), Argentina in 2004. He continued his studies at INRIA,France, funded by the FP6 FET integrated project ”MOBIUS: Mobility, Ubiquity and Security”, and received a Ph.D. from the Ecole des Mines de Paris (ENSMP), France in February, 2009. He joined the IMDEA Software Institute as a postdoctoral researcher in February 2009.
Cesar Sanchez (Home Page at IMDEA Software Institute)
César Sánchez joined the IMDEA Software Institute in 2008, after a short post-doc at University of California at Santa Cruz, USA. In 2009 he received a dual appointment as a at the Spanish National Research Council (CSIC). He received a Ph.D. in Computer Science from Stanford University, USAin 2007, and a M.S in Computer Science in 2001 also from Stanford University, USA. Before that, César received an MSEE (Ingeniería de Telecomunicación) from the Technical University of Madrid (UPM), Spain in 1998.
I am a researcher at the MSRC PPT group. My interests span programming languages theory and implementation, type systems, theorem proving, semantics, functional programming, and — of course — Haskell! I am involved in the design and implementation of the constraint solver underlying GHC’s type inference engine. I am also fascinated by using PL techniques such as program analyses or domain-specific languages to optimize systems.Francois Dupressoir (Home Page at IMDEA Software Institute)
François Dupressoir joined the IMDEA Software Institue as a postdoctoral researcher in February 2013. He successfully defended his Ph.D. in Computer Science at the Open University under the supervision of Andy Gordon, Jan Jürjens and Bashar Nuseibeh. His Ph.D. studies were partially funded by a Microsoft Research Ph.D. scholarship, and led him to intern at the European Microsoft Innovation Center, and at Microsoft Research in Redmond and Cambridge.
Georges Gonthier’s research interests include programming language design and semantics, concurrency theory and its application to security, and methods and tools for the formal verification of computer programs. One of his achievements on the latter subject is a fully checked formal proof of the famous Four Colour Theorem, using the Coq proof assistant developed at INRIA, the French Institut National de Recherche en Informatique et Automatique (this was work in collaboration with Benjamin Werner of INRIA).Gilles Barthe (Home Page at IMDEA Software Institute)
Gilles Barthe received a Ph.D. in Mathematics from the University of Manchester, UK, in 1993, and an Habilitation à diriger les recherches in Computer Science from the University of Nice, France, in 2004. He joined the IMDEA Software Institute in April 2008. Previously, he was head of the Everest team on formal methods and security at INRIA Sophia-Antipolis Méditerranée, France. He also held positions at the University of Minho, Portugal; Chalmers University, Sweden; CWI, Netherlands; University of Nijmegen, Netherlands. He has published more than 100 refereed scientific papers. He has been coordinator/principal investigator of many national and European projects, and served as the scientific coordinator of the FP6 FET integrated project “MOBIUS: Mobility, Ubiquity and Security” for enabling proof-carrying code for Java on mobile devices (2005-2009).
Ilya received a Ph.D. in Computer Science from iMinds-DistriNet research group at the Department of Computer Sciences of KU Leuven under supervision of Dave Clarke in November 2012. He joined IMDEA in February 2013. Before joining academia he worked as a software developer in JetBrains Inc.
I am a member of the Programming Principles and Tools group and lead the Verification and Automatic Reasoning Group. Most of my time is spent working on SLAyer, a formal verification tool aimed at ensuring correct use of dynamically-allocated heap memory. I’m also involved in the TERMINATOR project, where termination and other liveness properties are proved. Before joining MSR, I worked on Smallfoot, an automatic specification checking tool focused on the heap. I also talk to the SpaceInvader guys frequently.Madan Musuvathi (Home Page at Microsoft Research Redmond)
I am a Senior Researcher in the Research in Software Engineering group at Microsoft Research. My research focus is on scalable analysis of concurrent systems. More broadly, my interests include systems, program analysis, model checking, verification, and theorem proving. I spend a lot of time at Microsoft building analysis tools to improve the productivity of software developers and testers.
He received his Ph.D. from the University of New Mexico under the supervision of Deepak Kapur. He joined the IMDEA Software Institute as a postdoctoral researcher in June 2008 and after a temporary leave as a Visiting Researcher at Microsoft Research in Seattle he rejoined the Institute as a researcher in September 2010. His research interests are on developing practical techniques for modeling program behavior and using this information to support error detection and optimization applications. His work to date has focused on the development of static analysis for the program heap which infers region, sharing, footprint and heap based data-dependence information.Markulf Kohlweiss (Home Page at Microsoft Research Cambridge)
I am a researcher at Microsoft Research Cambridge in the Programming Principles and Tools group and a member of the Constructive Security sub group. I did my PhD at COSIC (Computer Security and Industrial Cryptography) group at the Department of Electrical Engineering ESAT of the K.U.Leuven. During my PhD I worked as a researcher in the European PRIME project (Privacy Enhancing Identity Management for Everyone) and PrimeLife project.
Mike Emmi currently holds a faculty researcher position at the IMDEA Software Institute. In 2010 he was awarded a Ph.D. from theDepartment of Computer Science at the University of California, Los Angeles (UCLA) under the advising of Dr. Rupak Majumdar, and from 2010 to 2012 he was a postdoctoral fellow of the Fondation Sciences Mathématiques de Paris,hosted by LIAFA, a laboratory of Université Paris Diderot (Paris 7). He has been a teaching assistant for undergraduate courses at UCLA and Université Paris Diderot, and has held internships at Microsoft Research, NASA Ames Research Center, and IBM
Nikhil Swamy (Home Page at Microsoft Research in Redmond)
I’m a Researcher in the RiSE group at MSR Redmond. My work covers various topics including type systems, program logics, functional programming, program verification and interactive theorem proving. I often think about how to use these techniques to build provably secure programs, including web applications, web browsers, crypto protocol implementations, and low-level systems code.
Pierre-Yves Strub received his Ph.D. in Computer Science from École Polytechnique, France, in 2008. He joined the IMDEA Software Institute in 2013, after a post-doctoral position at the Microsoft-INRIA Joint Lab in Paris, France and at the LIAMA institute in Beijing, China. Pierre-Yves research interests include formal proofs, proof assistants and their related type theory, certification of cryptographic algorithms and mathematical proofs, program verification via typing, secure web programming. He currently focused on EasyCrypt, a toolset for reasoning about relational properties of probabilistic computations with adversarial code. He is one of the main authors of EasyCrypt. He is also the main author of CoqMT, an extension of the Coq proof assistant.Santiago Zanella Béguelin (Home Page at Microsoft Research Cambridge)
I am a Post-Doctoral Researcher at Microsoft Research Cambridge, UK. I am a member of the Programming Principles and Tools and Constructive Security groups. I also collaborate with the Secure Distributed Computations and their Proofs team of the INRIA-Microsoft Research Joint Centre.Previously, I held a Post-Doctoral position at the Madrid Institute for Advanced Studies in Software Development Technologies (IMDEA Software Institute), Spain. Once upon a time I got my PhD from École Nationale Supérieure des Mines de Paris, working in the Everest and Marelle teams at INRIA Sophia Antipolis-Méditerranée, France, under the supervision of Gilles Barthe.
My research interest is the use of the shared memory programming paradigm to program distributed, parallel, or concurrent or systems conveniently, efficiently, and correctly. I am particularly interested in the following topics: Concurrent, Parallel, and Distributed Programming Models; Touch-enabled scripting languages for mobile+cloud; Relaxed Memory Models, Eventual Consistency, and Consistency in Distributed Systems; Verification and Debugging Tools for Concurrent Programs.
I am a member of the Research in Software Engineering group at Microsoft Research. My work aims to improve software reliability by providing programmers with automated tools to analyze their programs. Most of my work has focused on analysis of concurrent software.
I am Assistant Managing Director of Microsoft Research India, and “area champion” for two research areas in Microsoft Research India: (1) Programming Languages and Tools, (2) Security and Privacy
Simon Peyton Jones (Home Page at Microsoft Research Cambridge)
I’m a researcher at Microsoft Research in Cambridge, England. I started here in Sept 1998. I’m also an Honorary Professor of the Computing Science Department at Glasgow University, where I was a professor during 1990-1998.