To boost performance, modern transactional systems provide weaker consistency guarantees than those defined by serialisability. Such transactional systems exhibit subtle behaviours that make it difficult for programmers to write correct applications. This problem is complicated by the fact that consistency models specifications are often informal, or they use disparate formalisms.

I will present a framework for specifying transactional consistency model. Then I will focus on Snapshot Isolation, a well-known consistency model, and show how a thorough analysis of its formal specification leads to deriving a static analysis technique for performing transaction chopping under Snapshot Isolation.