Automatic test case generation is a key ingredient of an efficient and cost-effective software verification process. AutoBlackTest focuses on testing applications that interact with the users through a GUI, and generates test cases at the system level. AutoBlackTest uses reinforcement learning to learn how to interact with the application under test and stimulate its functionalities.

Click here for more information about AutoBlackTest


Automata Violations Analyzer, AVA, is a technique to automatically produce candidate interpretations of software failures from anomalies identified by anomaly detection techniques. Interpretations capture the rationale of the differences between legal and failing executions with user understandable patterns that simplify identification of failure causes. Empirical validation conducted both with synthetic cases and third-party systems showed that AVA produces useful interpretations.

Click here for more information about AVA


BCT is a tool that automatically identifies anomalous events that likely caused failures, filters the possible false positives, and presents the resulting data by building views that show chains of cause-effect relations, i.e., views that show when anomalous events are caused by other anomalous events. BCT comes with a library that provides its core functionality and an Eclipse plugin that provides management and visualization facilities.

Click here for more information about BCT


HEX is a logic for describing structural properties of program heaps. It can be used to express preconditions and data structure invariants for the analysis of software properties based on generalized symbolic execution.

Click here for more information about HEX


JBSE (the Java Bytecode Symbolic Executor) is a special-purpose Java virtual machine for the analysis of software. JBSE performs a very precise kind analysis called symbolic execution, based on the actual simulation of the program according to the Java Virtual Machine specification v.2. JBSE can be applied for assertion-based verification of software compiled to Java bytecode. Work is ongoing to extend the application of JBSE to automatic test case generation.

Click here for more information about JBSE


KLFA is a tool that automatically analyzes log files and retrieves important information to identify failure causes. KLFA automatically identifies dependencies between events and values in logs corresponding to legal executions, generates models of legal behaviors and compares log files collected during failing executions with the generated models to detect anomalous event sequences that are presented to users.

Click here for more information about KLFA


Link is a technique to automatically generate test cases for GUI-based applications that process complex data, such as maps, personal data, book information, travel data. The novel idea of Link is to exploit the Web of Data to generate test data that match the semantics of the related fields, and satisfy the semantic constraints that arise among interrelated fields. Link automatically analyzes the GUI of the application under test, queries Linked Data KBs to extract the data that can be used in the tests, and uses the extracted data to generate complex system test inputs.

The tool will be available soon. Please contact if you want to receive a notification email when the tool will be on-line.


The majority of IDEs implement a concept of plug-in that nicely supports the integration of tools within the IDEs. Plug-ins dramatically simplify the structural integration of multiple tools, but provide little support to the design of the dynamic of the integration, which must be entirely coded by programmers from plug-ins’ API. Manually integrating plug-ins is costly, complex and requires a deep understanding of the underlying environment. The implementation of tools as plug-ins and the integration of the results produced by different plug-ins are still difficult, expensive and error-prone activities. In our vision, IDE users must be able to execute plug-ins and integrate their results by designing workflows that can be persisted, executed and re-used in other workflows. MASH is an Eclipse plug-in that enable users to compose the functionality provided by different plug-ins at runtime, by drawing a workflow in their workspace.

Click here for more information about MASH


RADAR (Regression Analysis with Diff And Recording) is a technique for debugging regression faults. RADAR combines monitoring, model inference and anomaly detection into a solution for the automatic identification of the anomalous behaviors that caused a regression failure. RADAR is implemented as an Eclipse plug-in and allows developers to analyze failures directly in the Eclipse IDE. In particular, RADAR can visualize the chain of anomalous behaviors that caused a failure, and provide developers a rich set of dynamic data that can be used to understand the context of the failure.

Future versions of RADAR will leverage Grammatech CodeSurfer static analysis capabilities to precisely pinpoint the code changes that lead to the regression.

Click here for more information about RADAR