RiSE Working Group on Program Analysis

Established: December 7, 2011

The RiSE Working Group on Program Analysis (PAx) improves the productivity of developer and testers and the reliability and security of software systems via novel techniques and tools for program analysis, testing, and verification.

People

Publications

Projects

Duality

Established: February 7, 2012

Duality solves Relation Post-Fixed Point problems using Craig interpolation. In can be used, for example, to generate proofs for procedural programs in the form of procedure summaries. Duality is envisioned as a generic engine for program analysis, supporting applications such…

The F* Project

Established: March 25, 2011

F* is a verification-oriented dialect of ML. For more information, please visit https://fstar-lang.org or click on the logo below.

SymDiff: Differential program verifier

Established: October 14, 2010

SymDiff is an infrastructure for leveraging and extending program verification to reason about relationship between two programs (differential program analysis). There are several opportunities for differential analysis, including (a) performing incremental analysis, (b) use one program as a spec to…

Moles – Isolation framework for .NET

Established: January 25, 2010

Moles allows to replace any .NET method with a delegate. Moles supports static or non-virtual methods. Moles works well with Pex. The Fakes Framework in Visual Studio 2012 is the next generation of Moles & Stubs. Fakes is different…

Cuzz – Concurrency Fuzzing

Established: February 6, 2012

Cuzz is a very effective tool for finding concurrency bugs. Cuzz works on unmodified executables and is designed for maximizing concurrency coverage for your existing (unmodified) tests. It randomizes the thread schedules in a systematic and disciplined way, using an…

Dafny: A Language and Program Verifier for Functional Correctness

Established: December 23, 2008

Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative,…

Boogie: An Intermediate Verification Language

Established: December 10, 2008

Boogie is an intermediate verification language, 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 for…

VCC: A Verifier for Concurrent C

Established: December 10, 2008

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…

HAVOC

Established: November 25, 2008

HAVOC is a tool for specifying and checking properties of systems software written in C, in the presence of pointer manipulations, unsafe casts and dynamic memory allocation. The assertion logic of HAVOC allows the expression of properties of linked lists…

Code Contracts

Established: October 28, 2008

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to…

CHESS: Find and Reproduce Heisenbugs in Concurrent Programs

Established: October 1, 2008

CHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved…

Pex and Moles – Isolation and White box Unit Testing for .NET

Established: February 21, 2007

Pex automatically generates test suites with high code coverage using automated white box analysis. Pex is a Visual Studio add-in for testing .NET Framework applications. Moles supports unit testing by providing isolation by way of detours and stubs. The Moles…

Spec#

Established: June 11, 2004

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…