6 papers
Synthesizing Proofs Using Proof Sharding and Exploration
Seyed Armin Vakil Ghahani, Manos Kapritsos
Distributed systems are hard to implement correctly, and subtle bugs can go undetected using traditional testing. Formal verification offers an alternative for proving the correctn…
täkōFormal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version)
Pranav Srinivasan, Manos Kapritsos, Yatin A. Manerkar
Accelerators provide large performance and energy-efficiency benefits, but can significantly change the hardware-software interface. The täkō programmable memory hierarchy accelera…
Recipe: Hardware-Accelerated Replication Protocols
Dimitra Giantsidi, Emmanouil Giortamis, Julian Pritzi +3
Replication protocols are essential for distributed systems, ensuring consistency, reliability, and fault tolerance. Traditional Crash Fault Tolerant (CFT) protocols, which assume…
Picsou: Enabling Replicated State Machines to Communicate Efficiently
Reginald Frank, Micah Murray, Chawinphat Tankuranand +5
Replicated state machines (RSMs) cannot communicate effectively today as there is no formal framework or efficient protocol to do so. To address this issue, we introduce a new prim…
Formally verified asymptotic consensus in robust networks
Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin +2
Distributed architectures are used to improve performance and reliability of various systems. Examples include drone swarms and load-balancing servers. An important capability of a…
On the Significance of Consecutive Ballots in Paxos
Eli Goldweber, Nuda Zhang, Manos Kapritsos
In this paper we examine the Paxos protocol and demonstrate how the discrete numbering of ballots can be leveraged to weaken the conditions for learning. Specifically, we define th…