Research in Software Engineering (RiSE)
Downloads
Lean interactive theorem prover
May 2018
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 allows your focus to remain…
Boogie intermediate verification language
May 2018
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 for C and the verifiers…
P family of languages, compilers, and runtimes
November 2017
P family of languages, compilers and runtimes.
Code Contracts for .NET
March 2017
Source code for the CodeContracts tools for .NET Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs.
CCI (Common Compiler Infrastructure)
January 2017
CCI provides a rich infrastructure for working with .NET Assemblies: generating them from source, or rewriting them.
VCC
April 2016
VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program…
Automata
April 2015
Automata is a .NET library that provides algorithms for composing and analyzing regular expressions, automata, and transducers. In addition to classical word automata, it also includes algorithms for analysis of tree automata and tree transducers. The library covers algorithms over…
Microsoft Touch Develop
February 2015
Touch Develop is a touch-friendly, cross-platform, mobile-first app creation environment.