Microsoft Research Downloads

Z3 is an SMT solver that combines several theory solvers into a combined framework. It can be used to prove theorems and find counter-examples for non-theorems.

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. 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.

We provide a simple tool for combining photos with varying exposures into a single, well-balanced, high-dynamic-range photo.

Strings including before-and-after spelling-correction pairs in English and Japanese, derived automatically by processing keystroke logs collected through Amazon’s Mechanical Turk.

Detours is a library for intercepting arbitrary Win32 binary functions on x86 machines.

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.

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.

Proximal-gradient homotopy is an efficient numerical method for solving the L1-regularized least-squares problem—minimize_x (1/2) ||A*x-b||_2^2 + lambda*||x||_1—where A is an m-by-n matrix, and lambda is a positive regularization parameter. This method is especially effective for sparse recovery applications in which the dimensions satisfies m < n and the optimal solution x* is provably sparse. The implementation in MATLAB can solve the more general problem—minimize_x f(x) + lambda*R(x)—where f(x) is a differentiable convex function and R(x) is a simple convex function whose proximal mapping can be computed efficiently.

A still photograph is a limited format for capturing moments that span an interval of time. Video is the traditional method for recording durations of time, but the subjective “moment” that one desires to capture is often lost in the chaos of shaky camerawork, irrelevant background clutter, and noise that dominates most casually recorded video clips. Microsoft Research Cliplets is an interactive app that uses semi-automated methods to give users the power to create “cliplets”—a type of imagery that sits between stills and video from handheld videos. The tool provides a creative lens one can use to focus on important aspects of a moment by performing spatiotemporal compositing and editing on a video-clip input.

A still photograph is a limited format for capturing moments that span an interval of time. Video is the traditional method for recording durations of time, but the subjective “moment” that one desires to capture is often lost in the chaos of shaky camerawork, irrelevant background clutter, and noise that dominates most casually recorded video clips. Microsoft Research Cliplets is an interactive app that uses semi-automated methods to give users the power to create “cliplets”—a type of imagery that sits between stills and video from handheld videos. The tool provides a creative lens one can use to focus on important aspects of a moment by performing spatiotemporal compositing and editing on a video-clip input.

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 quickly can prototype new, high-speed wireless physical and media-access-control layers with a minimum of effort. Significant changes for this version include new BRICK model for baseband programming, user mode 802.11a sample, and a full new debug plot tool.

Infer.NET Fun turns the simple succinct syntax of F# into an executable modeling language. You can code up the conditional probability distributions of Bayes’ rule using F# array comprehensions with constraints. Write your model in F#. Run it directly to synthesize test datasets and to debug models. Or compile it with the Infer.NET compiler and runtime for efficient statistical inference.

The Microsoft Research Face SDK Beta for Windows Phone integrates the latest face technologies from Microsoft research teams. It provides state-of-the-art algorithms to process facial images such as face detection, alignment, tracking, and cartoon generation.

The grante library enables estimation and inference in discrete factor graph models using a variety of methods. It is a native C++ library but comes with a interface to Matlab. A detailed description of all supported methods is available in the archive.