Research in Software Engineering (RiSE)
Télécharger
Lean interactive theorem prover
mai 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
mai 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
novembre 2017
P family of languages, compilers and runtimes.
Code Contracts for .NET
mars 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)
janvier 2017
CCI provides a rich infrastructure for working with .NET Assemblies: generating them from source, or rewriting them.
VCC
avril 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
avril 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
février 2015
Touch Develop is a touch-friendly, cross-platform, mobile-first app creation environment.