Automatically find software defects without running the program using techniques such as deductive verification, model checking, abstract interpretation.
|
Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of pre-conditions, post-conditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking (via code rewriting), enable static contract verification (e.g. via abstract interpretation), and documentation generation. |
|
|
Spec# is a programming system aimed at improving the development and maintenance of correct software. It consists of the Spec# programming language (a superset of the object-oriented .NET language C#, adding non-null types and code contracts), the Spec# compiler (which emits run-time checks to enforce the contracts), and the Boogie-based static program verifier (which attempts to prove a program correct with respect to its contracts). |
|
|
HAVOC is a tool for specifying and checking properties of systems software written in C. The tool understands low-level pointer manipulations, internal pointers, and cast operations that are prevalent in systems software. The user provides annotates the program with specifications and HAVOC checks the annotated program modularly, one procedure at a time, using the Z3 automated theorem prover. |
|
|
Boogie is an intermediate verification language, designed to make the prescription of verification conditions natural and convenient. It serves as a common intermediate representation for static program verifiers of various source languages, and it abstracts over the interfaces to various theorem provers, including Z3. Boogie is the intermediate language for the program verifiers Spec#, HAVOC, and VCC. |
|
|
VCC stands for Verifying C Compiler. It 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. VCC also introduces claims, which are invariants that are preserved under concurrent modification. VCC's architecture follows the Spec# and Havoc pipeline: VCC translates C and contracts into BoogiePL, Boogie translates its input into formulas for Z3. |
|
|
SLAM is a joint research/development project for automated verification of C program against temporal safety properties. Groups involved are the SRR and RSE research groups, and the Windows Static Analysis for Drivers group. |
|
|
Software performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes to address the root cause before shipping). The SPEED project attempts to address these limitations by static estimation of symbolic computational complexity of programs. It builds over recent advances in static program analysis, which has traditionally been used for checking correctness as opposed to measuring performance. |
|
|
Dafny is an experimental language that explores the dynamic frames style of specifications in an object-based sequential setting. |
|
|
Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice. |
|
