Verifying a Realistic Mutable Hash Table
This work addresses verification of realistic mutable data structures for software reliability, though it is incremental as it builds on existing verification tools.
The researchers verified the mutable LongMap hash table from Scala's standard library using the Stainless verifier, fixing a bug for large tables and achieving performance within 1.5x of the original.
In this work, we verify the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array, using the Stainless program verifier. As a reference implementation, we write an immutable map based on a list of tuples. We then show that LongMap's operations correspond to operations of this association list. To express the resizing of the hash table array, we introduce a new reference swapping construct in Stainless. This allows us to apply the decorator pattern without introducing aliasing. Our verification effort led us to find and fix a bug in the original implementation that manifests for large hash tables. Our performance analysis shows the verified version to be within a 1.5 factor of the original data structure.