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