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.

• Code: https://github.com/peterzeller/repliss
• Demo: https://softech.cs.uni-kl.de/repliss/

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).

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

• Code: https://github.com/SyncFree/isabelle_crdt_verification

• Dissertation (preprint): Tool Supported Specification and Verification of Highly Available Applications
• Combining state- and event-based semantics to verify highly available programs (FACS 2019)
• Testing properties of weakly consistent programs with Repliss (PaPoC 2017)
  • Slides for PaPoC 2017
  • Slides for RainbowFS Workshop 2017
• FMKe: A Real-World Benchmark for Key-Value Data Stores (PaPoC 2017)
• Towards a Proof Framework for Information Systems with Weak Consistency (SEFM 2016)
• Formal Specification and Verification of CRDTs (FORTE 2014)
• Master’s Thesis: Specification and Verification of Convergent Replicated Data Types (Master’s Thesis)