PV0 Ceramist: Certified Approximate Membership StructuresCoq library for reasoning about Approximate Membership Query structures

Application domain/field

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

Last commit date

13 April 2020

Related papers

https://doi.org/10.1007/978-3-030-53291-8_16 (CAV '20)

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.