Comparing EventB, $\{log\}$ and Why3 Models of Sparse Sets
Software Engineering
2023-07-24 v2
Abstract
Many representations for sets are available in programming languages libraries. The paper focuses on sparse sets used, e.g., in some constraint solvers for representing integer variable domains which are finite sets of values, as an alternative to range sequence. We propose in this paper verified implementations of sparse sets, in three deductive formal verification tools, namely EventB, and Why3. Furthermore, we draw some comparisons regarding specifications and proofs.
Cite
@article{arxiv.2307.03974,
title = {Comparing EventB, $\{log\}$ and Why3 Models of Sparse Sets},
author = {Maximiliano Cristiá and Catherine Dubois},
journal= {arXiv preprint arXiv:2307.03974},
year = {2023}
}