Research in Software Engineering (RiSE)
다운로드
Lean interactive theorem prover
5월 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
5월 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
11월 2017
P family of languages, compilers and runtimes.
Code Contracts for .NET
3월 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)
1월 2017
CCI provides a rich infrastructure for working with .NET Assemblies: generating them from source, or rewriting them.
VCC
4월 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
4월 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
2월 2015
Touch Develop is a touch-friendly, cross-platform, mobile-first app creation environment.