Comparing EventB, $\{log\}$ and Why3 Models of Sparse Sets
Maximiliano Cristi\'a, Catherine Dubois
TL;DR
This paper presents verified implementations of sparse sets in EventB, log, and Why3, comparing their specifications and proofs to evaluate their effectiveness in formal verification contexts.
Contribution
It introduces verified sparse set implementations across three formal tools and compares their specifications and proof strategies.
Findings
Verified implementations in EventB, log, and Why3.
Comparison of specifications and proof processes.
Insights into formal verification of sparse sets.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Constraint Satisfaction and Optimization