Peter Zeller, M.Sc.

Photo of Peter Zeller, M.Sc.
Email p_zeller[at]
Phone +49 - 631 - 205 - 26 23
Fax +49 - 631 - 205 - 34 20
Postal address TU Kaiserslautern
Fachbereich Informatik, Gebäude 34
Postfach 30 49
D-67653 Kaiserslautern
Visitor address Gebäude 34, Raum 407
Zugang über Paul-Ehrlich-Str.
D-67653 Kaiserslautern


I am working on tools and techniques for building correct applications on top of databases, which provide only weak consistency guarantees.

Many databases choose a weak consistency model, because it enables low latency and high availability. However, programming becomes more difficult, if the foundation provides fewer guarantees. The goal of my research is to give programmers the techniques and tools required to ensure correctness of applications in this setting.


Repliss is a tool for developing correct applications on top of weakly consistent databases. The name is short for Replicated information systems with strong guarantees.

The tool features:

  • Automated testing
  • Automated verification
  • Manual verification (via Why3’s export to Isabelle)

Status: The tool is a research prototype, which is not yet documented.


Antidote is a replicated database featuring high availability, transactional causal+ consistency and expressive replicated data types.

I worked on the Antidote CRDT library, which features data types for managing replication and on client libraries (Erlang Client, JavaScript Client).

Verification of CRDTs

I verified some state based CRDTs using the Isabelle theorem prover.