Distributed Hash Tables are used as name-lookups in large decentralized distributed systems such as peer-to-peer networks and loosely connected machine clusters. Correctness is complicated by their distributed nature. This talk presents an implementation of one such DHT, written in Erlang, based on the Kademlia data structure. Its unique feature is that it comes equipped with a full QuickCheck specification, which semi-formally verifies its correct behaviour through random test generation.

The talk focuses on the test aspect of the system, and how one builds fairly large QuickCheck specifications for real-world systems, in particular by slicing a large specification into isolated parts and then reassembling those parts into a full model. It is intended to give people an overview of how to attack larger code bases with (semi-) formal methods.

Jesper Louis Andersen

Jesper Louis Andersen bridges the gap between theory and practice. He has a curiosity for programming language theory, math, and logic, but dabbles in many other fields of computer science as well. His main interest is to move state-of-the-art computer science research into real world use whenever possible. His dayjob involves functional programming for a danish startup.