Picture of Giuliano

Welcome to Giuliano's homepage!

(Some people also call me nano.)


You can contact me by email at giuliano@losa.fr

The fingerprint of my PGP key is D58B CCC5 28A5 F7CB 5B48 9CCF AE81 A995 EC2B 9EE4.

Current Situation

Since January 2017 I am working with with Eli Gafni at UCLA. On the more practical side, we are working on using ideas from distributed-computing theory to improve the design of distributed systems. On the more theoretical side, we are working on understanding distributed computing with deterministic objects, including 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 am working on increasing the applicability of replication, by implementing it in the operating system to achieve transparency; in the Hyflow project, I am working on improving the performance of geo-replication algorithms; finally, in continuation of my PhD research, I am investigating 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.

Recent Publications

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. To appear at 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.

PhD Thesis

I completed my PhD in February 2014, under the supervision of Rachid Guerraoui and Viktor Kuncak. The title of my thesis is "Modularity in the Design of Robust Distributed Algorithms". It is about structuring distributed algorithms in independent modes that can be analyzed in isolation, making the understanding of such algorithms much easier. I formalized my work and proved theorems about it with the interactive proof assistant Isabelle/HOL. I also use TLA+ and its model-checker TLC to test my specifications and eliminate many bugs in them.

PhD thesis

The TLA+ specifications appearing in my thesis

The Isabelle/HOL theories appearing in my thesis

A preliminary version of the work described in my thesis appeared in the paper: Guerraoui, Rachid, Viktor Kuncak, and Giuliano Losa. "Speculative linearizability", PLDI 2012. An updated version of the Isabelle/HOL theories can be found at the Archive of Forma Proofs, entry Abortable Linearizable Modules.