Giuliano Losa

Researcher in distributed computing and formal methods

Are specifications and proofs software?

python-fbas

A prototype tool to reason about Federated Byzantine Agreement Systems using SAT solvers. Sources are on github at https://github.com/nano-o/python-fbas.

Formalization and proof of a classical distributed algorithm

https://github.com/nano-o/Distributed-termination-detection

The algorithm is the “channel-counting” termination-detection algorithm of Kumar (1985). The proof I propose is a great example of inductive reasoning about distributed algorithms. The exercise branch of the repository sets things up as an exercise in finding inductive invariants.