About us

We are a team of researchers and engineers working to create state-of-the-art programming-by-example and other technologies for data wrangling and other application domains of program synthesis. This is a revolutionary charter since 99% of computer users lack programming skills, and data scientists spend 80% of their time wrangling with data. The team includes:

Sumit Gulwani leads the PROSE research & engineering team at Microsoft that develops program synthesis technologies for data wrangling and incorporates them into real products. Sumit’s programming-by-example work led to the Flash Fill feature in Microsoft Excel used by hundreds of millions of people. Sumit has co-authored around 50 patent applications, published 110 papers in top-tier conferences/journals across multiple computer science areas, and delivered 30 keynotes/invited talks at various forums. He was awarded the ACM SIGPLAN Robin Milner Young Researcher Award in 2014 for his pioneering contributions to end-user programming and intelligent tutoring systems. He obtained his PhD from UC-Berkeley, and was awarded the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his bachelor’s degree from IIT Kanpur in 2000, and was awarded the President’s Gold Medal.

Ranvijay has more than 18 years of experience in software industry and more than 10 years in managing product development. He is a BTech from IIT Kanpur (India) and has been a part of the founding team of three startups in the US and in India. Prior to joining Microsoft, Ranvijay managed the Research and new product development efforts of a Healthcare Product company based in Bellevue, Washington. He shipped a Health Information Exchange, a Healthcare Analytics Platform, and a Patient Master Data Management solution that uses advanced record linking capabilities to match Patient records across care settings. Ranvijay is very excited about the possibilities of Program Synthesis by Example technologies.

Vu obtained his PhD at the University of California, Davis in 2015, and his BEng at Vietnam National University in 2006. His PhD focuses on automatic program generation to help improve the quality of critical software and make programming more accessible to end users. His work has led to hundreds of bug reports/fixes in GCC and LLVM and important shipped features in Microsoft PowerShell and Operations Management Suite (Azure OMS). He is currently working on (predictive/by-example) text extraction, tree-based extraction and transformation, and predicate/conditional learning.

Daniel recently completed his PhD at the University of Washington working with Dan Grossman and Sumit Gulwani on program synthesis and is now a Research Software Engineer in the PROSE team. In addition to work on programming by example, his code has been deployed as the hint mechanism in MSR’s Code Hunt programming game.

Mark has been at Microsoft for 15 years, spending about half of that time in MSR. He graduated from Carnegie Mellon University and spent a year nearby working on certifying compilation and proof carrying code with Cedilla Systems. At Microsoft, he worked on Bartok, an optimizing ahead-of-time compiler and runtime system for C#, for a long time. As part of that work in MSR, he contributed to research in garbage collection, software transactional memory, and the Singularity managed OS project. He then worked on generics, separate compilation, and System C# as part of the Midori incubation effort. After a year and a half learning about Azure Storage, he is excited to have returned to the field of programming languages on the PROSE team.

Arjun is interested in the use of Formal Methods and Program Synthesis techniques to aid programmers in designing reliable and correct systems. Arjun graduated with a PhD from IST Austria in 2014, advised by Thomas A. Henzinger. His dissertation on the use of quantitative techniques in formal verification and synthesis was awarded the ACM SIGBED Paul Caspi Dissertation Award in recognition of an outstanding doctoral dissertation that significantly advances the state of the art in the science of embedded systems. During his stint as a Post-doctoral Researcher in the group of Rajeev Alur at the University of Pennsylvania, he developed novel divide-and-conquer program synthesis strategies. Syntax-guided Synthesis SyGuS solvers based on these strategies have won the SyGuS competition for two years running.

Mohammad’s background and interests are in formal methods for reasoning about computer programs. He holds a PhD in Computer Science from Imperial College London and a Masters in Mathematics from the University of Cambridge. He works on the development of techniques and tools for program synthesis through natural interaction paradigms such as programming by examples, natural language, or a combination of such approaches. In particular, he is interested in the applications of these techniques for data wrangling tasks such as extraction, formatting, cleaning, or transformations in various data formats including spreadsheets, text documents, and richly formatted documents. In the PROSE Team his current focus is on developing examples-based and fully automated synthesis technologies for information extraction from web pages.

Danny has worked in the software industry (both inside Microsoft and out) for over 25 years. He first started at Microsoft in 1997 working on the Outlook team, and then spent nearly 15 years alternating between shipping products like Excel, Live Meeting and the Entity Framework and participating in incubation efforts for very interesting technologies which usually didn’t ship in the form originally targeted. Outside of Microsoft he has worked as a Unix System Admin in the Idaho State University computer center, founded an early Internet Service Provider, helped INRIX with their traffic data web services, and served as CTO of a startup building RFID-based inventory tracking systems for small businesses, among other endeavors.

Abhishek graduated with a PhD from the University of Pennsylvania, in 2016, advised by Rajeev Alur. His dissertation explored techniques for synthesizing distributed protocols and loop-free programs. He has contributed to development of the SyGuS language definition, and has also developed SyGuS solvers which have been primarily based on enumerative program synthesis strategies. His research interests include formal methods and program synthesis, and he very much enjoys building systems to demonstrate the practicality of his research.

Titus’ research interests lie at the intersection of human-computer interaction and software engineering. He applies mixed-method approaches to understand difficulties practitioners face within the domains of software engineering, data science, and end-user programming. Within PROSE, Titus works closely with product teams at Microsoft to pinpoint opportunities to leverage program synthesis technology, and conducts usability and design research to learn how practitioners can more effectively interact with software tools.

Gustavo is a Researcher in the PROSE team. Previously, he was an Assistant Professor in the Department of Computing and Systems at the Federal University of Campina Grande (UFCG), Brazil, and worked as a postdoc at UC Berkeley with Bjoern Hartmann. He completed his PhD at UFCG under supervision of Rohit Gheyi in 2014. His research was awarded the ACM SIGPLAN John Vlissides Award and the CAPES Award for Best CS PhD Thesis in Brazil. Gustavo’s research interests include program synthesis, HCI, and software engineering. In the PROSE Team, his currently focused on developing techniques to perform tree transformations by example.

Alan Leung obtained his PhD in 2017 from the University of California, San Diego, where he was a member of the Programming Systems Group advised by Sorin Lerner. His dissertation investigated interactive program synthesis techniques for constructing parsers and lexers by example. Previously, he was a circuit design engineer at Intel, where he designed and implemented microprocessor caches. He holds a BS in Electrical and Computer Engineering from Cornell University.

Kunal Pathak started in Microsoft in 2009 after receiving a Masters in Computer Science from Rochester Institute of Technology. His specialization was in programming languages and developer tools. Prior joining PROSE team, he was part of Chakra team working on performance and memory optimization of the compiler. He was also part of an ambitious project to enable node.js to run with Chakra engine and earned the collaborator status of node.js repository. In PROSE team, Kunal works on devising techniques for generating efficient programs from PROSE framework, writing translators for various programming languages that the generated program can be serialized into and integration of PROSE technology with partners.

Ivan is a Researcher in the PROSE team. Previously, he was a research assistant at TU Wien (Formal Methods in Systems Engineering group), where he worked on applying formal methods and programming languages in programming education and cost analysis. Ivan’s research interests include program synthesis, programming languages, and software engineering.

Ashish Tiwari received his B.Tech degree in Computer Science from the Indian Institute of Technology, Kanpur in 1995, and his Ph.D. in Computer Science from the State University of New York at Stony Brook in 2000. He has published over 75 peer-reviewed research papers in the areas of formal methods, static program analysis, automated deduction, synthesis, hybrid systems, and symbolic computation. His work on automated abstractions of hybrid systems and program synthesis is widely cited. Dr. Tiwari has served as a PI or co-PI on several National Science Foundation (NSF) and National Aeronautics and Space Administration (NASA) funded grants. He was a Staff Scientist in the Formal Methods group of the Computer Science Laboratory at SRI International before joining the PROSE team.

Alumni