一句话：提出一种编译器方法，利用预定义数组性质自动验证含非线性索引的数据并行程序。
在函数式数据并行程序中，索引数组计算被分解为 map、前缀和、scatter 等批量并行算子，用于收集或散布数据数组元素，从而决定数据数组的性质。这种编程风格给通用验证框架（如 Dafny、F*、Liquid Haskell）带来困难：它们灵活强大，但需要冗长标注和非平凡的用户证明，非专家难以使用。本文提出一种编译器方法，以高自动化程度验证数组性质，旨在让不具备验证专业知识的数据并行程序用户也能使用验证。方法支持一组小而强大的预定义性质——等价性、范围、单射性、双射性、单调性、过滤、划分——使编译器能在更高抽象层次上自动推理。评估涵盖具有非线性索引的挑战性应用，包括图算法、Cooley-Tukey FFT、过滤、多路划分，以及难以验证的扁平化不规则嵌套并行程序（如对不同大小数组的批量操作）。
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.
@article{HinnerskovSO26,
title = {Verifying Array Properties in Pure Data-Parallel Programs},
author = {Nikolaj Hey Hinnerskov and Robert Schenck and Cosmin Oancea},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808304}
}