I am interested in distributed-systems analysis, design, and implementation aided by formal methods. For example, I have recently worked on formally verifying BFT-consensus algorithms such as Tendermint and the Stellar Consensus Protocol.
I work for the Stellar Development Foundation.
You can email me at giuliano at losa.fr for personal matters and at giuliano at stellar.org for work-related matters.
I also have a one-post blog on this website.
Recent publications and artifacts
- Semitopology: a new topological model of heterogeneous consensus
- Consensus in the Unknown-Participation Message-Adversary Model
- Cachin, Christian, Giuliano Losa, and Luca Zanolini. Quorum Systems in Permissionless Network (OPODIS 2020).
- Formal proof of the accountability property of Tendermint in Ivy, and a blog post briefly describing the project.
- A blog post on the on model-based testing of implementations of the QUIC protocol with Ivy, with Docker setup to replicate the results
- Giuliano Losa and Mike Dodds On the Formal Verification of the Stellar Consensus Protocol, FMBC 2020.
- Marta Lokhava, Giuliano Losa, David Mazières, Graydon Hoare, Nicolas Barry, Eliezer Gafni, Jonathan Jove, Rafał Malinowsky, Jed McCaleb. Fast and secure global payments with Stellar, SOSP 2019.
- Giuliano Losa, Eli Gafni, and David Mazières. Stellar Consensus by Instantiation, DISC 2019. Extended Version and additional material.
- Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham. Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. CAV 2019. Extended version
- Eli Daian, Giuliano Losa, Yehuda Afek and Eli Gafni. Deterministic Objects Give Life to Non-Deterministic 1-Consensus Tasks, DISC 2018 (also see this github repository).
- Marcelo Taube, Giuliano Losa, Kenneth McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos: Modularity for Decidability of Deductive Verification with Applications to Distributed Systems, PLDI 2018. Additional material here.
- Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham: Reducing Liveness to Safety in First-Order Logic, POPL 2018.
- Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, Giuliano Losa: The assignment problem, ICDCN 2018. Technical report and TLA+ specifications.
- Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham: Paxos Made EPR: Decidable Reasoning about Distributed Consensus, OOPSLA 2017. Technical report on arXiv.org and paper site at TAU with supplementary material.
- Balaji Arun, Sebastiano Peluso, Roberto Palmieri, Giuliano Losa, and Binoy Ravindran: Speeding up Consensus by Chasing Fast Decisions. 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN, June 26-29, 2017, Denver, CO, USA. Technical report.
- Giuliano Losa, Sebastiano Peluso, Binoy Ravindran: Brief Announcement: A Family of Leaderless Generalized-Consensus Algorithms, PODC 2016. PDF and TLA+ specifications.
- Sebastiano Peluso, Alexandru Turcu, Roberto Palmieri, Giuliano Losa, Binoy Ravindran: Making Fast Consensus Generally Faster, DSN 2016. PDF and TLA+ specifications.
FRIDA Workshop
I helped organize the 2021 Workshop on Formal Reasoning in Distributed Algorithms (FRIDA). You can find the videos of the talks on Youtube: Monday’s session and Friday’s session.
In 2020, Marijana Lazić and myself organized the "2020 Workshop on Formal Reasoning in Distributed Algorithms (FRIDA). You can find the videos of the talks on the QONFEST YouTube channel (search for FRIDA in video titles).