Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. In the presence of concurrent accesses, databases trade off isolation for performance. The weaker the isolation level, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors. However, these weak behaviors only occur rarely in practice and outside the control of the application, making it difficult for developers to check the robustness of their code against weak isolation levels.

In this talk I will present a framework for formalizing database isolation levels and algorithmic methods for checking whether a database conforms to a certain isolation level or that an application satisfies its intended specification when run under a given isolation level.