Research in Software Engineering (RiSE)

FStar Data Set v2

September 2024

This dataset is the Version 2.0 of the FStar Data Set. This dataset’s primary objective is to train and evaluate Proof-oriented Programming with AI (PoPAI, in short). Given a specification of a program and proof in F*, the objective of…

FStar Data Set v1

September 2024

This dataset contains programs and proofs in F* proof-oriented programming language. The data, proposed in Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming, is an archive of source code, build artifacts, and metadata assembled from eight different F⋆-based open source projects…

MicroCode

June 2024

Microsoft MicroCode is an icon-based programming language and editor for young learners to code with the BBC micro:bit V2. MicroCode allows you to program the micro:bit V2 with only an Arcade shield accessory – no other computer is required! If…

Koka

June 2021

Koka: a Functional Language with Effects Koka is a strongly typed functional-style language with effect types and handlers.

REST API Fuzz Testing

November 2020

This self-hosted service developed for Azure, including its orchestration engine and security tools (including MSR’s RESTler), enables developers to embed security tooling into their CI/CD workflows.

RESTler-Fuzzer

November 2020

RESTler is the first stateful REST API fuzzing tool for automatically testing cloud services through their REST APIs and finding security and reliability bugs in these services.

Bosque Programming Language

May 2019

The Bosque programming language is an experiment in regularized design for a machine-assisted rapid and reliable software development.

Z3 automated theorem prover

May 2018

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages including .NET, C, C++, Java, OCaml,…

F* language and verifier

May 2018