Share on Facebook Tweet on Twitter Share on LinkedIn Share by email


Seal is a modular static analysis tool that infers side-effects of methods in a .NET application. The side-effects of a method are the set of heap locations in the program state right before the invocation of the method (referred to as prestate) that are modified (or written) by the method. Intuitively, these are the locations on which the method has an effect and hence can be expected to change after the method invocation. A method with no side-effects is said to be pure. Seal supports many sophisticated (and higher-order) C# features such as LINQ, delegates, event-handlers, exceptions, and scales to several thousand lines of code. Check out Seal in action here.

Q Program Verifier

The Q program verifier is a collection of front-ends that compile different source languages to an intermediate representation (IR), and back-ends that perform verification on the IR. Together, Q is a verification platform that hosts multiple tools and technologies for analyzing properties of programs. Q stands out from its competition in its unique support for analyzing concurrent, multi-core, as well as distributed systems.


Holmes is a statistical tool that automatically finds the most likely cause of test failures. Holmes collects and analyzes fine-grained path coverage data and identified code paths that strongly correlate with failure. Holmes integrates right into Visual Studio code editor and supports analysis of both automated units tests and manual tests (run through Visual Studio Test Elements).


Yogi is a scalable software property checking tool. It systematically combines static analysis with testing. This synergy between testing and static analysis is harnessed to efficiently validate software.