Scalable Deductive Verification of Data-Level Parallel Programs

• URL: http://arxiv.org/abs/2605.13616v1
• Date: Wed, 13 May 2026 14:45:49 GMT
• Title: Scalable Deductive Verification of Data-Level Parallel Programs
• Abstract summary: We introduce a technique to rewrite expressions with (nested) quantifiers.<n>We also make reasoning about potentially overlapping arrays easier.<n>All our techniques are implemented in the VerCors program verifier.
• Score: 1.2999413717930817
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper introduces several techniques that improve the scalability of the deductive verification of data-level programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable triggers can be generated for these expressions. We have proven this rewrite technique correct in a theorem prover. Second, we make reasoning about potentially overlapping arrays easier, by providing specification constructs to indicate and verify that two arrays are not aliases, or that they are immutable, so they can be modelled as mathematical sequences. All our techniques are implemented in the VerCors program verifier. We illustrate how our techniques improve scalability through a large number of experiments. Using our techniques on a set of typical GPU kernels, we achieve a reduction of verification time by, on average, a factor of 9, with outliers being up to 150 times faster. Additionally, applying these techniques to earlier experiments and an earlier case study of a radio telescope pipeline permitted the verification of results which were previously unobtainable and significantly reduced the verification time.

Related papers

• Federated stochastic bilevel optimization with fully first-order gradients [57.1147486991903]
  Federated matrices bilevel optimization has been actively studied in recent years due to its widespread applications in machine learning.<n>Most existing federated bilevel optimization algorithms require the computation of second-order Hessian and Jacobian matrices.<n>We propose a novel federated convergence variance-reduced bilevel descent algorithm that relies solely on first-order oracles.
  arXiv  Detail & Related papers  (2026-09-14T21:12:59Z)
• Improving Algorithmic Efficiency using Cryptography [11.496343300483904]
  We show how to use cryptography to improve the time complexity of solving computational problems.<n>We show that under standard cryptographic assumptions, we can design algorithms that are determinantally faster than existing ones.
  arXiv  Detail & Related papers  (2025-02-18T17:08:59Z)
• Optimizing Tensor Computation Graphs with Equality Saturation and Monte Carlo Tree Search [0.0]
  We present a tensor graph rewriting approach that uses Monte Carlo tree search to build superior representation. Our approach improves the inference speedup of neural networks by up to 11% compared to existing methods.
  arXiv  Detail & Related papers  (2024-10-07T22:22:02Z)
• Parallel Decoding via Hidden Transfer for Lossless Large Language Model Acceleration [54.897493351694195]
  We propose a novel parallel decoding approach, namely textithidden transfer, which decodes multiple successive tokens simultaneously in a single forward pass. In terms of acceleration metrics, we outperform all the single-model acceleration techniques, including Medusa and Self-Speculative decoding.
  arXiv  Detail & Related papers  (2024-04-18T09:17:06Z)
• Stochastic Optimization for Non-convex Problem with Inexact Hessian Matrix, Gradient, and Function [99.31457740916815]
  Trust-region (TR) and adaptive regularization using cubics have proven to have some very appealing theoretical properties. We show that TR and ARC methods can simultaneously provide inexact computations of the Hessian, gradient, and function values.
  arXiv  Detail & Related papers  (2023-10-18T10:29:58Z)
• Learning the Positions in CountSketch [49.57951567374372]
  We consider sketching algorithms which first compress data by multiplication with a random sketch matrix, and then apply the sketch to quickly solve an optimization problem. In this work, we propose the first learning-based algorithms that also optimize the locations of the non-zero entries.
  arXiv  Detail & Related papers  (2023-06-11T07:28:35Z)
• CeFlow: A Robust and Efficient Counterfactual Explanation Framework for Tabular Data using Normalizing Flows [11.108866104714627]
  Counterfactual explanation is a form of interpretable machine learning that generates perturbations on a sample to achieve the desired outcome. State-of-the-art counterfactual explanation methods are proposed to use variational autoencoder (VAE) to achieve promising improvements. We design a robust and efficient counterfactual explanation framework, namely CeFlow, which utilizes normalizing flows for the mixed-type of continuous and categorical features.
  arXiv  Detail & Related papers  (2023-03-26T09:51:04Z)
• Toward Learning Robust and Invariant Representations with Alignment Regularization and Data Augmentation [76.85274970052762]
  This paper is motivated by a proliferation of options of alignment regularizations. We evaluate the performances of several popular design choices along the dimensions of robustness and invariance. We also formally analyze the behavior of alignment regularization to complement our empirical study under assumptions we consider realistic.
  arXiv  Detail & Related papers  (2022-06-04T04:29:19Z)
• Verify Linearizability of Concurrent Stacks [0.0]
  We propose a new proof technique for verifying linearizability of concurrent stacks.<n>We first prove the soundness of the elimination mechanism, a common optimization used in concurrent stacks.<n>We then present a stack theorem that reduces the problem of proving linearizability to establishing a set of conditions.
  arXiv  Detail & Related papers  (2021-10-12T07:52:37Z)
• Second-order Neural Network Training Using Complex-step Directional Derivative [41.4333906662624]
  We introduce a numerical algorithm for second-order neural network training. We tackle the practical obstacle of Hessian calculation by using the complex-step finite difference. We believe our method will inspire a wide-range of new algorithms for deep learning and numerical optimization.
  arXiv  Detail & Related papers  (2020-09-15T13:46:57Z)
• Kernel methods through the roof: handling billions of points efficiently [94.31450736250918]
  Kernel methods provide an elegant and principled approach to nonparametric learning, but so far could hardly be used in large scale problems. Recent advances have shown the benefits of a number of algorithmic ideas, for example combining optimization, numerical linear algebra and random projections. Here, we push these efforts further to develop and test a solver that takes full advantage of GPU hardware.
  arXiv  Detail & Related papers  (2020-06-18T08:16:25Z)
• Making Convolutions Resilient via Algorithm-Based Error Detection Techniques [2.696566807900575]
  Convolutional Neural Networks (CNNs) accurately process real-time telemetry. CNNs must execute correctly in the presence of hardware faults. Full duplication provides the needed assurance but incurs a 100% overhead.
  arXiv  Detail & Related papers  (2020-06-08T23:17:57Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. We propose a novel approach based on Lagrangian Decomposition. We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
  arXiv  Detail & Related papers  (2020-02-24T17:55:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.