Verifying Isolation Levels of Database Implementations for Free Using Separation Logic

Anders Alnor Mathiasen, Amin Timany, Lars Birkedal

Modern databases are highly concurrent and provide transactions as a mean of grouping several database operations into atomically applied units. Database vendors and software engin…