I am working at Galois in Porland, Oregon, on formal verification projects since April 2019. From January 2017 to February 2019 I was working with with Eli Gafni at UCLA as a postdoc. During my postdoc I was pursuing several research projects:
Permissionless Consensus using Quorum Systems. Thanks to a generous gift from the Stellar Foundation, I am working on the theory behind permissionless quorum systems and on formally verifying critical algorithms and software artifacts underlying the Stellar Network. This includes developing an IRTF Internet Draft about the Stellar Consensus Protocol
Formal Verification. My first research project is about developping methods and tools to allow practical development of formally verified systems software. In particular, I am exploring how decidable logics can be used in practice to formally verify systems software.
Theory of Distributed Computation. My second research project concerns that theory of distributed computation. It is to classify the synchronization power of deterministic objects. One immediate goal is to prove the conjectured robustness of the consensus hierachy.
I previously worked as a post-doc at Virginia Tech in the Systems Software Research Group. My research at Virginia Tech was about improving the reliability of software systems through replication techniques, on multiple fronts: in the Popcorn Linux project, I worked on implementing transparent replication of Linux application inside the Linux kernel; in the Hyflow project, I worked on improving the performance of geo-replication algorithms; finally, in continuation of my PhD research, I investigated how to effectively develop correct-by-construction distributed systems in the interactive theorem prover Isabelle/HOL.
Before joining Virginia Tech, I worked as a software engineer at ELCA, in Switzerland, where my colleagues and I developed a new encryption system for the Swiss inter-bank clearing network. I hold a PhD in Computer Science from EPFL, Switzerland.
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, to appear in 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.
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.
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.
The fingerprint of my PGP key is D58B CCC5 28A5 F7CB 5B48 9CCF AE81 A995 EC2B 9EE4.