Formal Specification and Verification of CRDTs. - Peter Zeller 001; Annette Bieniusa; Arnd Poetzsch-Heffter (FORTE, 2014)

Towards a Proof Framework for Information Systems with Weak Consistency. - Peter Zeller 001; Arnd Poetzsch-Heffter (SEFM, 2016)

FMKe: a Real-World Benchmark for Key-Value Data Stores. - Gonçalo Tomás; Peter Zeller 001; Valter Balegas; Deepthi Devaki Akkoorath; Annette Bieniusa; João Leitão 001; Nuno M. Preguiça (PaPoC@EuroSys, 2017)

Testing properties of weakly consistent programs with Repliss. - Peter Zeller 001 (PaPoC@EuroSys, 2017)

Collaborative Work Management with a Highly-Available Kanban Board. - Annette Bieniusa; Peter Zeller 001; Shraddha Barke (Principled Software Development, 2018)

Ensuring referential integrity under causal consistency. - Marc Shapiro 001; Annette Bieniusa; Peter Zeller 001; Gustavo Petri (PaPoC@EuroSys, 2018)

Combining State- and Event-Based Semantics to Verify Highly Available Programs. - Peter Zeller 001; Annette Bieniusa; Arnd Poetzsch-Heffter (FACS, 2019)

Szpilrajn Extension Theorem. - Peter Zeller 001 (Arch. Formal Proofs, 2019)

Teaching practical realistic verification of distributed algorithms in Erlang with TLA+. - Peter Zeller 001; Annette Bieniusa; Carla Ferreira 001 (Erlang Workshop, 2020)

Combining state- and event-based semantics to verify highly available applications. - Peter Zeller 001; Annette Bieniusa; Arnd Poetzsch-Heffter (Sci. Comput. Program., 2021)

Tool Supported Specification and Verification of Highly Available Applications. - Peter Zeller 001 (2021)