Research Tools: code, datasets, & models

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license (opens in new tab). Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for…

KreMLin is a tool that extracts an F* program to readable C code. If the F* program verifies against a low-level memory model that talks about the stack and the heap; if it is first-order;…

Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This…

Boogie is an intermediate verification language (IVL), intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers…

A Python package that implements a variety of algorithms that mitigate unfairness in supervised machine learning.

This is a Microsoft Visual Studio solution that contains reference implementation of the TPM 2.0 Specification by TCG available at https://trustedcomputinggroup.org/tpm-library-specification (opens in new tab). See the TPMCmd/tpm/include/TpmTypes.h header for the exact revision/date of the TPM…

The source code for the simulations in the paper, 007: Democratically Finding The Cause of Packet Drops (NSDI 2018). To run: use MultiFailureDriver or SingleLinkFailureDriver (these are the starting points/drivers of the code).

This is a small library for implementing several standard “test collection” or “offline” evaluation measures for search systems. See: https://github.com/Microsoft/irmetrics-r (opens in new tab)

This C library implements FrodoKEM, an IND-CCA secure key encapsulation (KEM) protocol based on the well-studied Learning with Errors (LWE) problem [1], which in turn has close connections to conjectured-hard problems on generic, “algebraically unstructured” lattices. FrodoKEM is…