Automated generator of library abstractions for scalable bug detection in large Java programs.
Aspect-oriented framework for Java bytecode instrumentation. Notable features include extensible pointcut model, efficient access to static and dynamic program context, and high degree of code coverage.
Endicheck is a Valgrind tool to help you detect missing byte-swaps in your program. Endicheck is distributed as a fork of Valgrind.
Portable research operating system based on microkernel multiserver design paradigms and built using fine-grained software components. HelenOS is flexible, modular, extensible, fault-tolerant and easy to understand.
HLAF provides high-level awareness based on data and fusion of data collected in the project and supports both offline and online decisions by offering insights in the data.
Panda is an extension for Java Pathfinder [1], which introduces support for predicate abstraction and various other abstractions of numeric data domains, such as signs and intervals. The name "Panda" stands for Predicate Abstraction in Dynamic Analysis.
SharpDetect is a dynamic analysis framework that enables observing and analyzing runtime behavior of .NET programs.
Multiplatform Java agent for hight-precision microbenchmarking that is able to
collect JVM events, data from hardware performance counters and strives to
have small performance overhead.
Archive
The goal of the Procasor Environment project is to develop an interactive environment for writing requirement specifications, where formal behavior specifications are created in paralel with textual use cases.
Vladimír Mencl
A generic coding pattern useful for implementing dynamic adaptation that selects the faster alternative at run-time.
COMBAT is a toolset for verification and analysis of behavior of software components that are implemented in Java. It supports the SOFA and Fractal component models, and assumes that the formalism of behavior protocols is used for specification of component behavior.
Environment Generator is a tool that allows to create an environment for a primitive component that is necessary for verification of the component with Java PathFinder.
Tool for testing OMG IDL compilers. Generates random IDL files of preset complexity together with code that uses the IDL compiler output. This helps check both parsing and code generation.
Java Pathfinder extension aimed at verification of Java programs for real-time and embedded platforms, such as RTSJ and SCJ.
Static analysis framework for web applications written in PHP. The aim of the framework is to allow easy specification of precise static analyses.