Here you find an overview of software, developed by our group.


Antidote is a planet scale, highly available, transactional database.


Repliss is a verification tool for information systems built on top of weakly consistent databases like Antidote.


Katja is a tool which generates rich Java libraries for order-sorted, immutable datatypes from concise specifications. Katja allows you to easily define immutable datatypes, which you can then use by adding a generated library to your system. It is a successor to the MAX tool developed by Arnd Poetzsch-Heffter. For more information consult the main Katja page.


jcobox150.png JCoBox is a programming language, which extends Java by a new concurrency concept, called CoBoxes. A compiler for JCoBox has been implemented and can be used to write concurrent Java programs using CoBoxes instead of threads and locks. For more information consult the main JCoBox page.

Backward Compatibility Verifier for Java Libraries

The Backward Compatibility Verifier is a tool which can verify that a newer implementation of a Java library is backward compatible to an older one. This means that every program that used the old version of the library should still work in the same way when using the new version of the library.


XCend (pronounced: TransCend) is a technology to specify and use hierarchical data structures. It is independent of any language or datatype paradigm, but - by using language dependent backends - code can be generated for various languages. The major benefit of XCend is the addition of integrity constraints to hierarchical data structures, which makes a XCend type more than the sum of its parts. The XCend technology then helps you in theoretically ensuring your data stays valid, but will also give you the ability to practically work with and manipulate your data nevertheless.

XCend has solid theoretical foundations, which are based on the interactive theorem prover Isabelle/HOL. More information about XCend can be found here, in particular the theory section and the extensive STATS example.


The STAT System is a handcrafted example system for XCend.

Further Tools

This page is currently under construction, so it does not represent a complete list, yet.