9 citations · 22 across the 10 of their papers we have counts for
1 paper · 1 filter
Niels Mündler, Tobias Nipkow
In this paper we present the verification of an imperative implementation of the ubiquitous B+-tree data structure in the interactive theorem prover Isabelle/HOL. The implementatio…