<

Martin Kleppmann

Distributed systems researcher and O'Reilly author

Dr Martin Kleppmann is a researcher in distributed systems at the University of Cambridge, and author of the acclaimed Designing Data-Intensive Applications┬Ł (O'Reilly Media, 2017). He mainly works on collaboration software, CRDTs, and formal verification of distributed algorithms.

Previously he was a software engineer and entrepreneur at Internet companies including LinkedIn and Rapportive, where he worked on large-scale data infrastructure.

Past Activities

Martin Kleppmann
Code Mesh LDN
08 Nov 2019
14.30 - 15.15

Correctness proofs of distributed systems with Isabelle

Testing systems is great, but tests can only explore a finite set of inputs and behaviours, while many distributed systems have an infinite state space. If you want to be sure that a program does the right thing in all possible situations, testing is not sufficient: only mathematical proof can cover an infinite state space. This talk introduces Isabelle/HOL, an interactive proof assistant (a kind of programming language and REPL for proofs), and explores how to formally verify distributed algorithms.

THIS TALK IN THREE WORDS

Distributed

Formal

Verification

OBJECTIVES

Attendees will:

  • Get a taste of why and how we can formally verify software and algorithms
  • Understand the most important reasoning tools available, such as proof by induction
  • Learn about the difference between proof assistants like Isabelle and model-checkers like TLA+

TARGET AUDIENCE

Software developers who have experience developing distributed systems, but who have not previously done any formal verification.