F* extends core-ML with a type system based on dependent refinements, higher kinds and affine types. It enables verification of higher-order stateful programs with automation via SMT solving.

Microsoft Research Mood Board is a Windows application that combines image search, image collection, and sketching to support creative activities.

Infer.NET is a framework for running Bayesian inference in graphical models.

Faster is not always better. With the Mañana Mail add-in for Outlook, you can send an e-mail at 9am with a single click, and you can edit or cancel it up until that point. It also gives you about ten seconds to undo sending any email. Research shows that important emails are often not urgent. Give yourself the chance to think it over, and let the recipients read it carefully at work instead of while they are distracted at dinner.

GeoS is a tool for semi-automated segmentation of 3D CT Scan imagery and other modalities.

A file-formats plug-in for the Mac version of Photoshop that enables the loading and saving of JPEGXR images.

A file-formats plug-in for Photoshop that enables the loading and saving of images in the JPEGXR format.

The Microsoft Research Software Radio (Sora) is a fully programmable software radio platform based on the commodity multicore CPU in a host PC. With Sora, researchers and engineers can quickly prototype new, high-speed wireless physical and media-access-control layers with a minimum of effort. Sora provides the BRICK model for baseband programming, user mode 802.11a sample, and a full new debug plot tool. Windows 7 is fully supported.

An integrated development environment for writing and checking TLA+ specifications.

An integrated development environment for writing and checking TLA+ specifications.

An integrated development environment for writing and checking TLA+ specifications.

An integrated development environment for writing and checking TLA+ specifications.

An integrated development environment for writing and checking TLA+ specifications.

An integrated development environment for writing and checking TLA+ specifications.

The TLA+ tool kit contains a) a parser and syntax checker for TLA+ specifications; b) a model checker and simulator for a subclass of "executable" TLA+ specifications; c) a program for typesetting TLA+ specifications; and d) a +Cal to TLA+ translator.

A library for programming Kinect for Windows inside Internet Explorer. This allows developers to write Web applications with Javascript that interface with the Kinect for Windows sytem.

The primary function of this add-in is to add a few buttons to the Outlook ribbon to prevent people from replying to all the recipients of your message or forwarding it, etc. The add-in uses a facility built into Outlook and Exchange that is more lightweight than information-rights management but is not exposed in the existing UI. The add-in also includes a check for common email errors, such as omitting attachments or subject lines.

This package contains the binaries necessary to use the Static Driver Verifier Research Platform with the Yogi verification engine.

SymDiff, a language-agnostic tool for equivalence checking and displaying semantic (behavioral) differences over imperative programs. The tool operates at the level of the intermediate verification language Boogie, and hence language-agnostic. This download contains a front end for comparing C programs compiled using the Microsoft C compiler.

SLAyer is an automatic, separation-logic-based memory safety checker. It checks that its input C code doesn't deference dangling pointers, do double frees, nor leak memory.

An updated version of Zing model checker.

Code accompanying the book: A. Criminisi, J. Shotton. Decision Forests for Computer Vision and Medical Image Analysis. Springer 2013. The code is provided so as to enable researcher to reproduce the toy examples in the book. This library contains a simplified implementation of decision forests and represents a good starting point for people who wish to learn about forests and how to implement them.

With this tool kit, users can mine linear temporal rules involving multiple events. The mined rules can capture data constraints on event fields and data-flow constraints between event fields via quantification. The tool kit can be used to mine rules over different views of events using event abstractions. In addition, the tool kit can be used to mine non-temporal rules involving single events, similar to frequent item sets. The tools operate on a well-defined, publicly available custom XML trace format....

The TPM Platform Crypto Provider and Toolkit contains sample code, utilities and documentation for using TPM-related functionality in Windows 8. Subsystems described include the TPM-backed Crypto-Next-Gen (CNG) platform crypto-provider, and how attestation-service providers can use the new Windows features. Both TPM1.2 and TPM2.0-based systems are supported.

This package contains an implementation of the "Decision Tree Fields" framework, described in the ICCV 2011 paper "Decision Tree Fields" by Nowozin, Rother, Bagon, Yao, Sharp, and Kohli. The DTF package allows training and testing of computer vision models for image labelling tasks such as image segmentation and semantic scene labelling.