7 papers
Extending Elle for Transaction Workloads with Duplicate Values
Zhiheng Cai, Si Liu, Hengfeng Wei +1
Elle is one of the most widely adopted black-box isolation validators. It crucially relies on the unique-value assumption for sound and efficient isolation validation. Yet, transac…
Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
Qiuhuan Xiong, Hengfeng Wei, Si Liu +2
Modern database systems widely support per-transaction isolation levels as a practical means of balancing consistency guarantees and performance. Yet, it remains largely unclear wh…
InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
Guangyuan Wu, Weining Cao, Zehui Tan +4
Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop…
Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
Weining Cao, Guangyuan Wu, Yuan Yao +3
Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved b…
Fast Verification of Strong Database Isolation (Extended Version)
Zhiheng Cai, Si Liu, Hengfeng Wei +2
Strong isolation guarantees, such as serializability and snapshot isolation, are essential for maintaining data consistency and integrity in modern databases. Verifying whether a d…
Boosting End-to-End Database Isolation Checking via Mini-Transactions (Extended Version)
Hengfeng Wei, Jiang Xiao, Na Yang +4
Transactional isolation guarantees are crucial for database correctness. However, recent studies have uncovered numerous isolation bugs in production databases. The common black-bo…