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

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.
J2BP is a tool for predicate abstraction of Java programs.
Light-weight computer simulator based on MIPS R4000.
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.
Static analysis framework for web applications written in PHP. The aim of the framework is to allow easy specification of precise static analyses.


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.
Practical verification using static analysis and Java Pathfinder
Java Pathfinder extension aimed at verification of Java programs for real-time and embedded platforms, such as RTSJ and SCJ.