DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
AD1105967
Title:
QUELEA: Verified Implementation of Weakly-Consistent Distributed Programs
Report Date:
2020-08-01
Abstract:
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.
Document Type:
Conference:
Journal:
Pages:
59
File Size:
2.28MB
FA8750-17-1-0006
(FA87501710006);
Contracts:
Grants:
Distribution Statement:
Approved For Public Release
