Verifying a Sparse Matrix Algorithm Using Symbolic Execution

• URL: http://arxiv.org/abs/2510.13424v1
• Date: Wed, 15 Oct 2025 11:23:32 GMT
• Title: Verifying a Sparse Matrix Algorithm Using Symbolic Execution
• Authors: Alexander C. Wilton,
• Abstract summary: We outline how symbolic execution can be used to write tests similar to traditional unit tests.<n>We provide stronger verification guarantees and apply this methodology to a sparse matrix algorithm.
• Score: 51.56484100374058
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Scientific software is, by its very nature, complex. It is mathematical and highly optimized which makes it prone to subtle bugs not as easily detected by traditional testing. We outline how symbolic execution can be used to write tests similar to traditional unit tests while providing stronger verification guarantees and apply this methodology to a sparse matrix algorithm.

Related papers

• Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances [44.0167033148715]
  We propose a novel parallel algorithm for decomposing hard CircuitSAT instances.<n>Our approach is implemented as a parameterized parallel algorithm, where adjusting the parameters allows efficient identification of high-quality decompositions.
  arXiv  Detail & Related papers  (2026-02-19T07:05:48Z)
• Block encoding of sparse matrices with a periodic diagonal structure [67.45502291821956]
  We provide an explicit quantum circuit for block encoding a sparse matrix with a periodic diagonal structure.<n>Various applications for the presented methodology are discussed in the context of solving differential problems.
  arXiv  Detail & Related papers  (2026-02-11T07:24:33Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
  arXiv  Detail & Related papers  (2025-10-03T16:21:14Z)
• CASET: Complexity Analysis using Simple Execution Traces for CS* submissions [0.0]
  The most common method to auto-grade a student's submission in a CS1 or a CS2 course is to run it against a pre-defined test suite and compare the results against reference results. This technique cannot be used if the correctness of the solution goes beyond simple output, such as the algorithm used to obtain the result. We propose CASET, a novel tool to analyze the time complexity of algorithms using dynamic traces and unsupervised machine learning.
  arXiv  Detail & Related papers  (2024-10-20T15:29:50Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  Uncertainty quantification is a key element of machine learning applications.<n>We introduce a novel benchmark that implements a collection of state-of-the-art UQ baselines.<n>We conduct a large-scale empirical investigation of UQ and normalization techniques across eleven tasks, identifying the most effective approaches.
  arXiv  Detail & Related papers  (2024-06-21T20:06:31Z)
• Learning to sample fibers for goodness-of-fit testing [0.0]
  We consider the problem of constructing exact goodness-of-fit tests for discrete exponential family models.<n>We translate the problem into a Markov decision process and demonstrate a reinforcement learning approach for learning good moves' for sampling.<n>Our algorithm is based on an actor-critic sampling scheme, with provable convergence.
  arXiv  Detail & Related papers  (2024-05-22T19:33:58Z)
• Precise Error Rates for Computationally Efficient Testing [67.30044609837749]
  We revisit the question of simple-versus-simple hypothesis testing with an eye towards computational complexity.<n>An existing test based on linear spectral statistics achieves the best possible tradeoff curve between type I and type II error rates.
  arXiv  Detail & Related papers  (2023-11-01T04:41:16Z)
• Test Primitive:A Straightforward Method To Decouple March [0.3535583356641669]
  This paper proposes a new test primitive for analyzing the March algorithm. The test primitives describe the common features that must be possessed for the March algorithm to detect corresponding faults.
  arXiv  Detail & Related papers  (2023-08-30T03:18:34Z)
• FastDiagP: An Algorithm for Parallelized Direct Diagnosis [64.65251961564606]
  FastDiag is a typical direct diagnosis algorithm that supports diagnosis calculation without predetermining conflicts. We propose a novel algorithm, so-called FastDiagP, which is based on the idea of speculative programming. This mechanism helps to provide consistency checks with fast answers and boosts the algorithm's runtime performance.
  arXiv  Detail & Related papers  (2023-05-11T16:26:23Z)
• Genetic Algorithms for Redundancy in Interaction Testing [0.6396288020763143]
  Interaction testing involves designing a suite of tests, which guarantees to detect a fault if one exists among a small number of components interacting together. Existing algorithms for constructing these test suites usually involve one "fast" algorithm for generating most of the tests, and another "slower" algorithm to "complete" the test suite. We employ a genetic algorithm that generalizes these approaches that also incorporates redundancy by increasing the number of algorithms chosen, which we call "stages"
  arXiv  Detail & Related papers  (2020-02-13T10:16:46Z)

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.