1 citations · 3 across the 5 of their papers we have counts for
5 papers
Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions
Shabnam Ghasemirad, Christoph Sprenger, Si Liu +1
We present a mathematically rigorous, systematic approach for the verification of database isolation guarantees, which (i) supports a spectrum of seven isolation levels, (ii) uncov…
VerIso: Verifiable Isolation Guarantees for Database Transactions
Shabnam Ghasemirad, Si Liu, Christoph Sprenger +2
Isolation bugs, stemming especially from design-level defects, have been repeatedly found in carefully designed and extensively tested production databases over decades. In paralle…
Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
Shabnam Ghasemirad, Christoph Sprenger, Si Liu +2
Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxe…
Protocols to Code: Formal Verification of a Next-Generation Internet Router
João C. Pereira, Tobias Klenze, Sofia Giampietro +8
We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in…
Formal Verification of the Sumcheck Protocol
Azucena Garvía Bosshard, Jonathan Bootle, Christoph Sprenger
The sumcheck protocol, introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems in computational complexity theory and cryptography,…