Declarative Distributed Systems (DDSs) are distributed systems grounded in logic programming. Although DDS model-checking is undecidable in general, we detect decidable cases by tweaking the data-source bounds, the message expressiveness, and the channel type.
@article{arxiv.2308.10007,
title = {Verification of Sometimes Termination of Lazy-Bounded Declarative Distributed Systems},
author = {Francesco Di Cosmo},
journal= {arXiv preprint arXiv:2308.10007},
year = {2023}
}
Comments
Published in the online proceedings of the ESSLLI 2021 Student Session