Projects
Established:
Machine learning, in particular Large Language Models, has shown great promise at automating several aspects of programming and software development such as coding, testing, integration, static analysis, verification etc. in recent years. In this project, we leverage and extend large…
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:
Connect and code electronics. Instantly. Jacdac (opens in new tab) is an open source hardware/software platform that makes it easy for everyone to create custom electronic solutions from a wide variety of hardware devices, (opens in new tab)with standardized PCB-based…
Established:
An efficient SMT solver Z3 is an efficient Satisfiability Modulo Theories (SMT) solver from Microsoft Research. Z3 is a solver for symbolic logic, a foundation for many software engineering tools. SMT solvers rely on a tight integration of specialized engines…
Can we empower more people to build low-cost, custom accessibility devices? Over 1 billion people around the world have some form of disability and nearly everyone will experience disability at some point in their lifetime. No disability is alike. Everyone…
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:
Currently, developing new electronic devices requires significant expertise and resource, and such hardware products are often only practical at scale. We want to make the design and manufacture of new electronic devices quicker, cheaper, easier and more accessible. We feel…
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.
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…