Following tools are currently actively maintained and developed by our students and staff.

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.
J2BP is a tool for predicate abstraction of Java programs.
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.
Java Pathfinder extension aimed at verification of Java programs for real-time and embedded platforms, such as RTSJ and SCJ.
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.
Static analysis framework for web applications written in PHP. The aim of the framework is to allow easy specification of precise static analyses.

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
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.
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.
Practical verification using static analysis and Java Pathfinder