Program
Verification
Book
Homepage
All tools
PV0
PV1
PV2
PV3
PV4
PV5
PV6
Frameworks
Tags
Specification formats
About
PV0
⊧
Ceramist: Certified Approximate Membership Structures
Coq library for reasoning about Approximate Membership Query structures
Application domain/field
Probabilistic data structures
Approximate Membership Query structures (AMQs)
Type of tool
Library
Internals
Uses
Coq
,
MathComp
,
Infotheo
Comments
Coq-based mechanised framework, specialised for reasoning about Approximate Membership Query structures (AMQs), implemented as a
Coq
library AMQs -> probabilistic data structures that compactly implement (multi-)sets via hashing
Library
Links
Repository:
https://github.com/certichain/ceramist
Last commit date: 13 Apr 2020 (default branch)
Last commit date: 13 Apr 2020 (last activity)
Artifact:
https://zenodo.org/record/3749474
Related papers
Certifying Certainty and Uncertainty in Approximate Membership Query Structures
(CAV '20)
Last publication date
14 July 2020
ProVerB specific
Markdown description:
view/edit
Reason for this entry:
CAV 2020
Contained in the ProVerB22 dataset (
paper
+
artefact
)
ProVerB
is a part of
SLEBoK
. Last updated:
February 2023
.
