4 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…
Reachability Analysis of the Domain Name System
Dhruv Nevatia, Si Liu, David Basin
The high complexity of DNS poses unique challenges for ensuring its security and reliability. Despite continuous advances in DNS testing, monitoring, and verification, protocol-lev…