Strong isolation guarantees, such as serializability and snapshot isolation, are essential for maintaining data consistency and integrity in modern databases. Verifying whether a database upholds its claimed guarantees is increasingly critical, as these guarantees form a contract between the vendor and its users. However, this task is challenging, particularly in black-box settings, where only observable system behavior is available and often involves uncertain dependencies between transactions. In this paper, we present VeriStrong, a fast verifier for strong database isolation. At its core is a novel formalism called hyper-polygraphs, which compactly captures both certain and uncertain transactional dependencies in database executions. Leveraging this formalism, we develop sound and complete encodings for verifying both serializability and snapshot isolation. To achieve high efficiency, VeriStrong tailors SMT solving to the characteristics of database workloads, in contrast to prior general-purpose approaches. Our extensive evaluation across diverse benchmarks shows that VeriStrong not only significantly outperforms state-of-the-art verifiers on the workloads they support, but also scales to large, general workloads beyond their reach, while maintaining high accuracy in detecting isolation anomalies.

翻译：强隔离性保证（如可串行化与快照隔离）对于维护现代数据库的数据一致性与完整性至关重要。验证数据库是否遵循其宣称的保证日益关键，因为这些保证构成了供应商与用户之间的契约。然而，该任务极具挑战性，尤其在黑盒场景下，仅能获取可观测的系统行为，且常涉及事务间不确定的依赖关系。本文提出VeriStrong，一种用于强数据库隔离性的快速验证器。其核心是一种称为超多图的新型形式化方法，能够紧凑地捕捉数据库执行中确定与不确定的事务依赖关系。基于此形式化方法，我们开发了用于验证可串行化与快照隔离的可靠且完备的编码方案。为实现高效率，VeriStrong针对数据库工作负载特性定制了SMT求解策略，与先前通用方法形成对比。我们在多样化基准测试中的广泛评估表明，VeriStrong不仅在支持的工作负载上显著优于现有先进验证器，还能扩展到超出其处理范围的大型通用工作负载，同时在检测隔离异常方面保持高准确度。