https://arxiv.org/api/VW00eUaXsv2fnj7r3iyfdYEV2qA 2026-06-30T12:52:17Z 9958 1890 15 http://arxiv.org/abs/2312.02664v3 2025-01-20T10:51:49Z

The tensor notation used in several areas of mathematics is a useful one, but it is not widely available to the functional programming community. In a practical sense, the (embedded) domain-specific languages (DSLs) that are currently in use for tensor algebra are either 1. array-oriented languages that do not enforce or take advantage of tensor properties and algebraic structure or 2. follow the categorical structure of tensors but require the programmer to manipulate tensors in an unwieldy point-free notation. A deeper issue is that for tensor calculus, the dominant pedagogical paradigm assumes an audience which is either comfortable with notational liberties which programmers cannot afford, or focus on the applied mathematics of tensors, largely leaving their linguistic aspects (behaviour of variable binding, syntax and semantics, etc.) for the reader to figure out by themselves. This state of affairs is hardly surprising, because, as we highlight, several properties of standard tensor notation are somewhat exotic from the perspective of lambda calculi. We bridge the gap by defining a DSL, embedded in Haskell, whose syntax closely captures the index notation for tensors in wide use in the literature. The semantics of this EDSL is defined in terms of the algebraic structures which define tensors in their full generality. This way, we believe that our EDSL can be used both as a tool for scientific computing, but also as a vehicle to express and present the theory and applications of tensors.

2023-12-05T11:09:54Z 42 pages, 11 figures. Accepted for publication in the Journal of Functional Programming Jean-Philippe Bernardy Patrik Jansson http://arxiv.org/abs/2501.11252v1 2025-01-20T03:32:55Z

Logic bugs are bugs that can cause database management systems (DBMSs) to silently produce incorrect results for given queries. Such bugs are severe, because they can easily be overlooked by both developers and users, and can cause applications that rely on the DBMSs to malfunction. In this work, we propose Constant-Optimization-Driven Database Testing (CODDTest) as a novel approach for detecting logic bugs in DBMSs. This method draws inspiration from two well-known optimizations in compilers: constant folding and constant propagation. Our key insight is that for a certain database state and query containing a predicate, we can apply constant folding on the predicate by replacing an expression in the predicate with a constant, anticipating that the results of this predicate remain unchanged; any discrepancy indicates a bug in the DBMS. We evaluated CODDTest on five mature and extensively-tested DBMSs-SQLite, MySQL, CockroachDB, DuckDB, and TiDB-and found 45 unique, previously unknown bugs in them. Out of these, 24 are unique logic bugs. Our manual analysis of the state-of-the-art approaches indicates that 11 logic bugs are detectable only by CODDTest. We believe that CODDTest is easy to implement, and can be widely adopted in practice.

2025-01-20T03:32:55Z Proc. ACM Manag. Data 3, 1 (SIGMOD), Article 24 (February 2025), 24 pages Chi Zhang Manuel Rigger 10.1145/3709674 http://arxiv.org/abs/2501.11001v1 2025-01-19T10:14:57Z

Reverse engineering tools are required to handle the complexity of software products and the unique requirements of many different tasks, like software analysis and visualization. Thus, reverse engineering tools should adapt to a variety of cases. Static Code Analysis (SCA) is a technique for analyzing and exploring software source code without running it. Manual review of software source code puts additional effort on software developers and is a tedious, error-prone, and costly job. This paper proposes an original approach (called ScaMaha) for Object-Oriented (OO) source code analysis and visualization based on SCA. ScaMaha is a modular, flexible, and extensible reverse engineering tool. ScaMaha revolves around a new meta-model and a new code parser, analyzer, and visualizer. ScaMaha parser extracts software source code based on the Abstract Syntax Tree (AST) and stores this code as a code file. The code file includes all software code identifiers, relations, and structural information. ScaMaha analyzer studies and exploits the code files to generate useful information regarding software source code. The software metrics file gives unique metrics regarding software systems, such as the number of method access relations. Software source code visualization plays an important role in software comprehension. Thus, ScaMaha visualizer exploits code files to visualize different aspects of software source code. The visualizer generates unique graphs about software source code, like the visualization of inheritance relations. ScaMaha tool was applied to several case studies from small to large software systems, such as drawing shapes, mobile photo, health watcher, rhino, and ArgoUML. Results show the scalability, performance, soundness, and accuracy of ScaMaha tool. Evaluation metrics, such as precision and recall, demonstrate the accuracy of ScaMaha ...

2025-01-19T10:14:57Z 20 pages, 16 figures, 3 tables, 8 listings, and 90 references International Journal of Computing and Digital Systems, vol. 17, no. 1, pp. 1-20, 2025 Ra'Fat Al-Msie'deen 10.12785/ijcds/1571046420 http://arxiv.org/abs/2208.14739v5 2025-01-18T18:26:51Z

The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem opened for more than 20 years.

2022-08-31T09:39:46Z Logical Methods in Computer Science, Volume 21, Issue 1 (January 22, 2025) lmcs:9987 Emmanuel Hainry Bruce M. Kapron Jean-Yves Marion Romain Péchoux 10.46298/lmcs-21(1:5)2025 http://arxiv.org/abs/2501.10802v1 2025-01-18T15:51:27Z

Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. This paper gives a formal proof of security and correctness for a library that generates authenticated versions of data structures automatically. The proof is based on a new relational separation logic for reasoning about programs that use collision-resistant cryptographic hash functions. This logic provides a basis for constructing two semantic models of a type system, which are used to justify how the library makes use of type abstraction to enforce security and correctness. Using these models, we also prove the correctness of several optimizations to the library and then show how optimized, hand-written implementations of authenticated data structures can be soundly linked with automatically generated code. All of the results in this paper have been mechanized in the Coq proof assistant using the Iris framework.

2025-01-18T15:51:27Z Simon Oddershede Gregersen Chaitanya Agarwal Joseph Tassarotti http://arxiv.org/abs/2501.10668v1 2025-01-18T06:22:28Z

Existing precise pointer tracing methods introduce substantial runtime overhead to the program being traced and are applicable only at specific program execution points. We propose MappedTrace that leverages compiler-generated read-only maps to accurately identify all pointers in any given snapshot of a program's execution state. The maps record the locations and types of pointers, allowing the tracer to precisely identify pointers without requiring the traced program to maintain bookkeeping data structures or poll at safe points, thereby reducing runtime overhead. By running the tracer from a different address space or machine, MappedTrace presents new opportunities to improve memory management techniques like memory leak detection and enables novel use cases such as infinite memory abstraction for resource-constrained environments.

2025-01-18T06:22:28Z Zhiyao Ma Caihua Li Lin Zhong http://arxiv.org/abs/2501.10560v1 2025-01-17T21:30:55Z

Ensuring the proper use of sensitive data in analytics under complex privacy policies is an increasingly critical challenge. Many existing approaches lack portability, verifiability, and scalability across diverse data processing frameworks. We introduce Picachv, a novel security monitor that automatically enforces data use policies. It works on relational algebra as an abstraction for program semantics, enabling policy enforcement on query plans generated by programs during execution. This approach simplifies analysis across diverse analytical operations and supports various front-end query languages. By formalizing both data use policies and relational algebra semantics in Coq, we prove that Picachv correctly enforces policies. Picachv also leverages Trusted Execution Environments (TEEs) to enhance trust in runtime, providing provable policy compliance to stakeholders that the analytical tasks comply with their data use policies. We integrated Picachv into Polars, a state-of-the-art data analytics framework, and evaluate its performance using the TPC-H benchmark. We also apply our approach to real-world use cases. Our work demonstrates the practical application of formal methods in securing data analytics, addressing key challenges.

2025-01-17T21:30:55Z Haobin Hiroki Chen Hongbo Chen Mingshen Sun Chenghong Wang XiaoFeng Wang http://arxiv.org/abs/2501.09667v1 2025-01-16T17:05:41Z

Quantum gates are the fundamental instructions of digital quantum computers. Current programming languages, systems, and software development toolkits identify these operational gates by their titles, which requires a shared understanding of their meanings. However, in the continuously developing software ecosystem surrounding quantum computing -- spanning high-level programming systems to low-level control stacks -- this identification process is often error-prone, challenging to debug, maintenance-heavy, and resistant to change. In this paper, we propose replacing this nominal gate representation with a functional one. We introduce the OpenQudit system for describing, parsing, optimizing, analyzing, and utilizing programs comprising gates described as symbolic unitary expressions. As part of this effort, we design the Qudit Gate Language (QGL), a unitary-specific expression language, and implement a differentiating just-in-time compiler in OpenQudit towards embedding this language in quantum programming languages and systems. Additionally, we have precisely designed and implemented the Qudit Virtual Machine (QVM) to evaluate quantum programs and their gradients efficiently. This evaluation is performed millions of times during the compilation of quantum programs. Our QVM can compute gradients approximately ten times faster than current leading numerical quantum compilation frameworks in the most common use cases. Altogether, the OpenQudit system is envisioned to (1) support many-level or qudit-based quantum systems, (2) enable the safe composition of program transformation tools, (3) accelerate circuit optimizers and transpilers, (4) enable compiler extensibility, and (5) provide a productive, simple-to-use interface to quantum practitioners.

2025-01-16T17:05:41Z Ed Younis http://arxiv.org/abs/2411.14284v2 2025-01-16T16:31:25Z

Kleene Algebra with Tests (KAT) provides an elegant algebraic framework for describing non-deterministic finite-state computations. Using a small finite set of non-deterministic programming constructs (sequencing, non-deterministic choice, and iteration) it is able to express all non-deterministic finite state control flow over a finite set of primitives. It is natural to ask whether there exists a similar finite set of constructs that can capture all deterministic computation. We show that this is not the case. More precisely, the deterministic fragment of KAT is not generated by any finite set of regular control flow operations. This generalizes earlier results about the expressivity of the traditional control flow operations, i.e., sequential composition, if-then-else and while.

2024-11-21T16:34:53Z Balder ten Cate Tobias Kappé 10.1145/3704861 http://arxiv.org/abs/2411.13220v2 2025-01-16T16:17:00Z

Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as goto, break, and return. To overcome these limitations, we introduce Control-Flow GKAT (CF-GKAT), a system that allows reasoning about programs that include non-local control flow as well as hardcoded values. CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the nearly-linear efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT's abilities, we validated the output of several highly non-trivial program transformations, such as Erosa and Hendren's goto-elimination procedure and the output of Ghidra decompiler. CF-GKAT opens up the application of Kleene Algebra to a wider set of challenges, and provides an important verification tool that can be applied to the field of decompilation and control-flow transformation.

2024-11-20T11:28:23Z Cheng Zhang Tobias Kappé David E. Narváez Nico Naus 10.1145/3704857 http://arxiv.org/abs/2501.09430v1 2025-01-16T09:58:34Z

Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid π-calculus (HpC), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The π-calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The HpC we propose is a conservative extension of the classical π-calculus, i.e., the extension is ``minimal'', and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the HpC by considering a realistic handover protocol among mobile devices.

2025-01-16T09:58:34Z The published version of this article will be available in the ACM Digital Library as part of the Proceedings of the ACM on Programming Languages issue for SPLASH/OOPSLA 2025. This extended version contains additional appendices, proofs and case studies Xiong Xu Jean-Pierre Talpin Shuling Wang Hao Wu Bohua Zhan Xinxin Liu Naijun Zhan http://arxiv.org/abs/2411.15368v2 2025-01-16T05:40:08Z

Motivation: Automated bug detection in dynamically typed languages such as Python is essential for maintaining code quality. The lack of mandatory type annotations in such languages can lead to errors that are challenging to identify early with traditional static analysis tools. Recent progress in deep neural networks has led to increased use of neural bug detectors. In statically typed languages, a type checker is integrated into the compiler and thus taken into consideration when the neural bug detector is designed for these languages. Problem: However, prior studies overlook this aspect during the training and testing of neural bug detectors for dynamically typed languages. When an optional type checker is used, assessing existing neural bug detectors on bugs easily detectable by type checkers may impact their performance estimation. Moreover, including these bugs in the training set of neural bug detectors can shift their detection focus toward the wrong type of bugs. Contribution: We explore the impact of type checking on various neural bug detectors for variable misuse bugs, a common type targeted by neural bug detectors. Existing synthetic and real-world datasets are type-checked to evaluate the prevalence of type-related bugs. Then, we investigate how type-related bugs influence the training and testing of the neural bug detectors. Findings: Our findings indicate that existing bug detection datasets contain a significant proportion of type-related bugs. Building on this insight, we discover integrating the neural bug detector with a type checker can be beneficial, especially when the code is annotated with types. Further investigation reveals neural bug detectors perform better on type-related bugs than other bugs. Moreover, removing type-related bugs from the training data helps improve neural bug detectors' ability to identify bugs beyond the scope of type checkers.

2024-11-22T22:29:37Z Accepted by ICSE'25 Research Track Boqi Chen José Antonio Hernández López Gunter Mussbacher Dániel Varró http://arxiv.org/abs/2501.09225v1 2025-01-16T01:15:21Z

Advances in incremental Datalog evaluation strategies have made Datalog popular among use cases with constantly evolving inputs such as static analysis in continuous integration and deployment pipelines. As a result, new logic programming debugging techniques are needed to support these emerging use cases. This paper introduces an incremental debugging technique for Datalog, which determines the failing changes for a \emph{rollback} in an incremental setup. Our debugging technique leverages a novel incremental provenance method. We have implemented our technique using an incremental version of the Soufflé Datalog engine and evaluated its effectiveness on the DaCapo Java program benchmarks analyzed by the Doop static analysis library. Compared to state-of-the-art techniques, we can localize faults and suggest rollbacks with an overall speedup of over 26.9$\times$ while providing higher quality results.

2025-01-16T01:15:21Z David Zhao Pavle Subotic Mukund Raghothaman Bernhard Scholz 10.1017/S147106842500002X http://arxiv.org/abs/2501.09201v1 2025-01-15T23:24:32Z

The rise of automated code generation tools, such as large language models (LLMs), has introduced new challenges in ensuring the correctness and efficiency of scientific software, particularly in complex kernels, where numerical stability, domain-specific optimizations, and precise floating-point arithmetic are critical. We propose a stepwise semantics lifting approach using an extended SPIRAL framework with symbolic execution and theorem proving to statically derive high-level code semantics from LLM-generated kernels. This method establishes a structured path for verifying the source code's correctness via a step-by-step lifting procedure to high-level specification. We conducted preliminary tests on the feasibility of this approach by successfully lifting GPT-generated fast Fourier transform code to high-level specifications.

2025-01-15T23:24:32Z Accepted at the Theory and Practice of Static Analysis Workshop (TPSA), in conjunction with the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2025 Naifeng Zhang Sanil Rao Mike Franusich Franz Franchetti http://arxiv.org/abs/2403.16689v3 2025-01-14T21:37:31Z

This paper addresses the problem of preference learning, which aims to align robot behaviors through learning user specific preferences (e.g. "good pull-over location") from visual demonstrations. Despite its similarity to learning factual concepts (e.g. "red door"), preference learning is a fundamentally harder problem due to its subjective nature and the paucity of person-specific training data. We address this problem using a novel framework called SYNAPSE, which is a neuro-symbolic approach designed to efficiently learn preferential concepts from limited data. SYNAPSE represents preferences as neuro-symbolic programs, facilitating inspection of individual parts for alignment, in a domain-specific language (DSL) that operates over images and leverages a novel combination of visual parsing, large language models, and program synthesis to learn programs representing individual preferences. We perform extensive evaluations on various preferential concepts as well as user case studies demonstrating its ability to align well with dissimilar user preferences. Our method significantly outperforms baselines, especially when it comes to out of distribution generalization. We show the importance of the design choices in the framework through multiple ablation studies. Code, additional results, and supplementary material can be found on the website: https://amrl.cs.utexas.edu/synapse

2024-03-25T12:23:39Z Accepted (oral) at AAAI 25 Sadanand Modak Noah Patton Isil Dillig Joydeep Biswas