@article{10.1145/3808304,
author = {Hinnerskov, Nikolaj Hey and Schenck, Robert and Oancea, Cosmin},
title = {Verifying Array Properties in Pure Data-Parallel Programs},
year = {2026},
issue_date = {June 2026},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {10},
number = {PLDI},
url = {https://doi.org/10.1145/3808304},
doi = {10.1145/3808304},
abstract = {In functional data-parallel programs, index array computations are separated into sequences of bulk-parallel operators—map, prefix sum, scatter—and used to gather or scatter data array elements, thus determining data array properties. This programming style is problematic for general-purpose verification frameworks (e.g., Dafny, F*, Liquid Haskell), which are flexible and powerful, but require verbose annotations and non-trivial user proofs, making them inaccessible to non-experts. We present a compiler approach to verifying array properties with high automation, aimed at making verification of data-parallel programs more accessible to users without verification expertise. We support a small but powerful predefined set of properties—equivalence, range, injectivity, bijectivity, monotonicity, filtering, partitioning—that enable the compiler to (automatically) reason at a higher level of abstraction. We evaluate our approach on challenging applications with non-linear indexing, including graph algorithms, Cooley-Tukey FFT, filtering, multi-way partitioning, and flattened irregular nested parallel programs that are difficult to verify, such as batch operations on arrays of different sizes.},
journal = {Proc. ACM Program. Lang.},
month = jun,
articleno = {226},
numpages = {27},
keywords = {Array programming, data parallelism, irregular nested parallelism}
}