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…
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…
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: a Functional Language with Effects Koka is a strongly typed functional-style language with effect types and handlers.
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 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.
The Bosque programming language is an experiment in regularized design for a machine-assisted rapid and reliable software development.
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 several programming languages including .NET,…
