rise4fun - from Microsoft Research

software engineering tools from Microsoft Research

all tutorial automata concurrency design infrastructure languages security testing verification

Automatic Graph Layout

Agl is built on the principle of the Sugiyama scheme; it produces so called layered, or hierarchical layouts. This kind of a layout naturally applies to graphs with some flow of information.

A domain specific language for writing common string functions, combined with state of the art analysis

With BEK, you can answer questions like Do these two programs output the same string? Can this program ever output a target string? What happens if I compose these two programs? Does the order matter? More general than regular expressions, BEK has been specifically tailored to capture common idioms in string manipulating functions.

Intermediate Verification Language

Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages.

A language and program verifier for reasoning about concurrent programs.

Chalice is a simple imperative programming language with constructs for thread creation, locking, and channels. The language has built-in specification constructs, and specifications are written in the style of implicit dynamic frames with fractional permissions.

Language agnostic modular program verification and repair with abstract interpretation.

Code Contracts provide a language-agnostic solution to the problem of software specification and validation. They consist of an API (part of .NET) to author contracts, and several tools consuming it (e.g., code documentation, runtime checking, and static checking). The static checker, based on abstract interpretation, infers semantic facts and uses them to prove contracts, programmer-provided and language assertions. Furthermore, it helps the development process by providing verified code repairs.

Theorem-prover for Counterfactual Datalog

Counterdog is an automated theorem-prover for a counterfactual meta-logic about propositional Datalog programs. It is useful, for example, for reasoning about Datalog-based trust management and authorization languages.

A language and program verifier for functional correctness

Dafny is an imperative, object-oriented programming language with classes and inductive datatypes, and specification constructs for describing intended behavior. The Dafny verifier checks that programs live up to their specifications.

Distributed Knowledge Authorization Language

DKAL is a logic-based distributed authorization policy language. Originally it was aimed for authorization policies, but in fact it is appropriate for policies in general. In DKAL world, principals have their own states and compute their own knowledge. DKAL facilitates the analysis of policies. Are the given policies consistent? Do they comply with various regulations? Is privacy protected? And so on.

Empirical Software Engineering and Measurement Group

Esm focus on understanding various software development issues from an empirical perspective. We are involved in doing practical studies on large software systems.

Programming language combining functional, object-oriented and scripting programming.

F# is ideal for data-rich, concurrent and algorithmic development: 'simple code to solve complex problems'. F# is a simple and pragmatic programming language combining functional, object-oriented and scripting programming.

A verification tool for higher-order stateful programs

F* is a new ML-like programming language. It also works as a general-purpose verification tool for higher-order stateful programs. It is based on (and subsumes) two prior projects from MSR: Fine and F7.

Formal Modeling Using Logic Programming and Analysis

FORMULA is a modern formal specification language targeting model-based development (MBD). It is based on algebraic data types (ADTs) and strongly-typed constraint logic programming (CLP), which support concise specifications of abstractions and model transformations. Around this core is a set of composition operators for composing specifications in the style of MBD.

A function-oriented language with effect inference

Koka is a function-oriented programming language that seperates pure values from side-effecting computations. Koka has many features that help programmers to easily change their data types and code organization correctly, while having a small language core with a familiar JavaScript like syntax.

Runtime heap abstraction

Abstraction and visualization of heaps

Automatic test generation using Dynamic Symbolic Execution for .NET

Pex finds interesting input-output values of your methods, which you can save as a small test suite with high code coverage. Pex is used as the backend of the pex4fun game. In pex4fun, a player has to discover a secret program by inspecting of input and outputs generated by Pex.

Poirot is a tool for checking assertions in concurrent programs

concurrent revisions

Parallel and Concurrent Programming With Snapshots

Revisions provides programmers with a simple, yet powerful and efficient mechanism to execute various application tasks in parallel even if those tasks access the same data and may exhibit read-write or write-write conflicts. Revisions is based on mutable snapshots and deterministic conflict resolution.

Regular Expression Exploration

Rex turns regular expressions into Symbolic Automatons and applies state of art technique to generate members.

Side-Effects AnalysiS

A static analysis that determines the side-effects of a method

Automatic formal verification for programs with heaps.

SLAyer is an automatic, separation-logic-based memory safety checker. It checks that its input C code doesn't deference dangling pointers, do double frees, nor leak memory.

A formal language for API contracts

Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading.

Program your phone on your phone.

TouchDevelop is a new programming environment and language built around touch devices. Its typed, structured programming language is built around the idea of only using a touchscreen as the input device to author code. It has built-in primitives which make it easy to access the rich sensor data available on a mobile device. The state of the program is automatically distributed between mobile clients and the cloud, with automatic synchronization of data and execution between clients and cloud.

A Verifier for Concurrent C

VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity.

Efficient Theorem Prover

Z3 is a high-performance theorem prover. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers.

Python interface for the Z3 Theorem Prover

Z3 is a high-performance theorem prover. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers.

SMT-based Analysis of Biological Computation

Z3-4Bio provides a unified semantic framework based on transition systems which allows translations from a range of formalisms and tools for modeling biological systems to SMT encodings usable within the Z3 solver. With Z3-4Bio, a set biological questions that are hard to study using simulation can be aksed, and models can be analyzed formally against rich temporal specifications.