I am a software developer interested in:
- software correctness (formal verification and automated testing)
- tooling for software development (compiler and IDE development)
- distributed systems and concurrency
I developed the Repliss verification tool as part of my PhD thesis. It is a prototype for verifying highly available information systems that are built on top of weakly consistent databases such as Antidote.
I contributed to Antidote, a highly available distributed database with support for transactions and replicated data types (CRDTs).
I verified some CRDTs in Isabelle/HOL
I wrote prototypes of testing libraries to test some ideas regarding API design.
- https://github.com/peterzeller/java-smallcheck An implementation of SmallCheck for Java
- https://github.com/peterzeller/smallcheck4scala An implementation of SmallCheck for Scala (forked and extended from https://github.com/dwhjames/smallcheck4scala)
- https://github.com/peterzeller/dorEr An Erlang library for testing stateful systems with randomized tests with a more intuitive API than QuickCheck or Proper.
- https://github.com/peterzeller/go-stateful-test A Go library for testing stateful systems with randomized (QuickCheck) and exhaustive (SmallCheck) tests. This combines some learnings from the older testing libraries above.
- https://github.com/peterzeller/go-fun Functional data structures for Go.
I wrote a code generator for classes representing abstract syntax trees, which can be used for building compilers.
A Scala implementation of Wadlers pretty printing algorithm.
A Scala library for evaluating logical formulas with quantifiers using a simple narrowing technique.
I am one of the two inventors and core developers of the Wurst programming language.