Research Tools: code, datasets, & models

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…

This download contains the graphs (parsed source code) for the open-source projects used in the ICLR 2018 paper “Learning to Represent Programs with Graphs”. In this work, we present how to construct graphs from source…