QUELEA: Verified Implementation of Weakly-Consistent Distributed Programs

The Quelea project was centered on the development of language abstractions, database technologies, compilers, program analyses, verification techniques, and runtime systems for building scalable applications intended to operate in geo-distributed environments where issues of data consistency and visibility are significant and subtle. The most significant contributions of this project are: 1. program logics for reasoning about geo-replicated distributed data stores and distributed transactions; 2. automated verification techniques for proving the safety of applications executing in such environments; 3. model-checking techniques that increase the assurance of applications that are equipped with sophisticated safety invariants; 4. language design principles that yield correct-by-construction distributed applications; and, 5. testing frameworks that can automatically discover invariant violations with greater specificity than random testing approaches collectively validate the thesis underlying the proposed effort.