Projects
AI at Scale is an applied research initiative that works to evolve Microsoft products with the adoption of deep learning for both natural language text and image processing. Our work is actively being integrated into Microsoft products, including Bing, Office,…
Established:
Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. VeriSol (Verifier for Solidity) is a project for advancing the state-of-the-art in formal specification and verification of blockchain smart contracts, with the goal of bringing the technology…
Established:
CHET is a compiler and runtime that automates many parts of this process for neural network inference tasks. The compiler applies transformations based on a framework of symbolic analysis passes.
We aim to develop practical tools and techniques that can help cloud developers adequately debug, test, configure, and monitor their systems. The research spans all aspects of improving reliability and availability of large-scale cloud systems, including understanding various runtime failures…
Established:
We are revisiting the problem of safe program merge and conducting research towards eliminating bad merges (including merge conflicts) of any form by exploring and combining techniques from program verification (for precise formulation of correctness), program synthesis (for automating repeated…
Established:
Angelic verification (AV) brings the benefits of static assertion checking to production software without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize static assertion checking for…
Established:
Project Parade is a novel approach to parallelizing a large class of seemingly sequential applications wherein dependencies are, at runtime, treated as symbolic values.
Project Everest aims to build and deploy a verified HTTPS stack, constructing a high-performance, standards-compliant, and verified implementation of the full HTTPS ecosystem.