Research in Software Engineering (RiSE)
The RiSE group builds the system and foundations of programming through open-ended fundamental research in formal methods, high-performance computing, programming languages, and software engineering. We collectively work towards a future where computing systems are provably correct, secure, and performant. Our research synergistically combines symbolic reasoning, AI, and human-centric methods to empower every programmer and organization to achieve more.
Our research falls into the following thrusts:
Natural Specifications
We believe that future programming systems will allow humans to specify their intent naturally with the computer distilling this intent interactively into a precise formal specification. Towards this end, we are conducting research in the intersection of formal reasoning and natural-language processing to synthesize specifications from several natural artefacts: documentation, code, runtime traces, etc.
TAPP (opens in new tab), TiCoder (opens in new tab), TOGA (opens in new tab), NL2Post (opens in new tab), 3DGen (opens in new tab), Prompts are Programs (opens in new tab)
Verified Programming
Over the past decade, we have made huge strides in developing proof-oriented programming methodologies for building provably correct systems. For instance, verified parsers from our group now validates every packet in Azure to provably eliminate entire classes of security vulnerabilities. We are using AI advances to significantly increase the scope of proof-oriented programming and accelerate the development of provably correct systems.
Project Everest (opens in new tab), EverParse (opens in new tab), AutoParse, Verus, Pulse, Kuiper
Verified Configurations
Correctness of systems crucially depends on their configurations; misconfigurations, as equally as program bugs, can lead to serious reliability and security issues. We have long used symbolic reasoning methods to detect configuration errors in production systems; for instance, Azure makes more than 5 billion calls to our configuration verification tool every day and generates tens to thousand alerts that would otherwise could result in serious outages. We are developing methods to automatically infer intent to accelerate the verification of configurations.
High-Performance Computing & AI Infrastructure
We are developing state-of-the art high-performance computing and compiler techniques to improve the performance of our AI infrastructure. Programming abstractions and high-performance kernels developed by our group are used to serve production AI workloads in Azure.
MSCCL (opens in new tab), MSCCL++ (opens in new tab), CuSync (opens in new tab), FastKron (opens in new tab), TritonComm, Guidance (opens in new tab)
Formal Methods & Automated Reasoning
Our research is firmly rooted in formally reasoning about the correctness and performance of systems. To this end, we invest in long-term foundational research in formal methods and automated reasoning.
Programming Languages & Systems
We develop core programming language abstractions to improve the productivity of programmers everywhere.
F* (opens in new tab), Koka (opens in new tab), Azure Durable Functions (opens in new tab), Netherite (opens in new tab), Orleans (opens in new tab), Microsoft MakeCode (opens in new tab), Jacdac (opens in new tab), MSAGL-JS (opens in new tab), GenAIScript (opens in new tab)