Peter Zeller, M.Sc.
|Phone||+49 - 631 - 205 - 26 23|
|Fax||+49 - 631 - 205 - 34 20|
|Postal address||TU Kaiserslautern
Fachbereich Informatik, Gebäude 34
Postfach 30 49
|Visitor address||Gebäude 34, Raum 407
Zugang über Paul-Ehrlich-Str.
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.
Verification of CRDTs
I verified some state based CRDTs using the Isabelle theorem prover.
- Combining state- and event-based semantics to verify highly available programs (FACS 2019)
- Testing properties of weakly consistent programs with Repliss (PaPoC 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)