Certifying certainty and uncertainty in approximate membership query structures
From MaRDI portal
Publication:2226742
DOI10.1007/978-3-030-53291-8_16zbMATH Open1478.68160arXiv2004.13312OpenAlexW3042912077MaRDI QIDQ2226742
Publication date: 9 February 2021
Abstract: Approximate Membership Query structures (AMQs) rely on randomisation for time- and space-efficiency, while introducing a possibility of false positive and false negative answers. Correctness proofs of such structures involve subtle reasoning about bounds on probabilities of getting certain outcomes. Because of these subtleties, a number of unsound arguments in such proofs have been made over the years. In this work, we address the challenge of building rigorous and reusable computer-assisted proofs about probabilistic specifications of AMQs. We describe the framework for systematic decomposition of AMQs and their properties into a series of interfaces and reusable components. We implement our framework as a library in the Coq proof assistant and showcase it by encoding in it a number of non-trivial AMQs, such as Bloom filters, counting filters, quotient filters and blocked constructions, and mechanising the proofs of their probabilistic specifications. We demonstrate how AMQs encoded in our framework guarantee the absence of false negatives by construction. We also show how the proofs about probabilities of false positives for complex AMQs can be obtained by means of verified reduction to the implementations of their simpler counterparts. Finally, we provide a library of domain-specific theorems and tactics that allow a high degree of automation in probabilistic proofs.
Full work available at URL: https://arxiv.org/abs/2004.13312
Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Randomized algorithms (68W20) Formalization of mathematics in connection with theorem provers (68V20)
Uses Software
This page was built for publication: Certifying certainty and uncertainty in approximate membership query structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226742)
