Journal: Proceedings of the ACM on Programming Languages

Abbreviation

Proc. ACM Program. Lang.

Publisher

Association for Computing Machinery

Journal Volumes

ISSN

2475-1421

Description

Filters

2018 - 201992020 - 202669
Reset filters

Search Results

Publications1 - 10 of 78
  • API-Driven Program Synthesis for Testing Static Typing Implementations
    Item type: Journal Article
    Sotiropoulos, Thodoris; Chaliasos, Stefanos; Su, Zhendong (2024)
    Proceedings of the ACM on Programming Languages
    We introduce a novel approach for testing static typing implementations based on the concept of API-driven program synthesis. The idea is to synthesize type-intensive but small and well-typed programs by leveraging and combining application programming interfaces (APIs) derived from existing software libraries. Our primary insight is backed up by real-world evidence: a significant number of compiler typing bugs are caused by small test cases that employ APIs from the standard library of the language under test. This is attributed to the inherent complexity of the majority of these APIs, which often exercise a wide range of sophisticated type-related features. The main contribution of our approach is the ability to produce small client programs with increased feature coverage, without bearing the burden of generating the corresponding well-formed API definitions from scratch. To validate diverse aspects of static typing procedures (i.e., soundness, precision of type inference), we also enrich our API-driven approach with fault-injection and semantics-preserving modes, along with their corresponding test oracles. We evaluate our implemented tool, Thalia on testing the static typing implementations of the compilers for three popular languages, namely, Scala, Kotlin, and Groovy. Thalia has uncovered 84 typing bugs (77 confirmed and 22 fixed), most of which are triggered by test cases featuring APIs that rely on parametric polymorphism, overloading, and higher-order functions. Our comparison with state-of-the-art shows that Thalia yields test programs with distinct characteristics, offering additional and complementary benefits.
  • Fractional Resources in Unbounded Separation Logic
    Item type: Conference Paper
    Dardinier, Thibault; Müller, Peter; Summers, Alexander J. (2022)
    Proceedings of the ACM on Programming Languages
    Many separation logics support fractional permissions to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes. Fractional permissions extend to composite assertions such as (co)inductive predicates and magic wands by allowing those to be multiplied by a fraction. Typical separation logic proofs require that this multiplication has three key properties: it needs to distribute over assertions, it should permit fractions to be factored out from assertions, and two fractions of the same assertion should be combinable into one larger fraction. Existing formal semantics incorporating fractional assertions into a separation logic define multiplication semantically (via models), resulting in a semantics in which distributivity and combinability do not hold for key resource assertions such as magic wands, and fractions cannot be factored out from a separating conjunction. By contrast, existing automatic separation logic verifiers define multiplication syntactically, resulting in a different semantics for which it is unknown whether distributivity and combinability hold for all assertions. In this paper, we present a novel semantics for separation logic assertions that allows states to hold more than a full permission to a heap location during the evaluation of an assertion. By reimposing upper bounds on the permissions held per location at statement boundaries, we retain key properties of separation logic, in particular, the frame rule. Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools and enjoys distributivity, factorisability, and combinability. We have formalised our semantics and proved its properties in Isabelle/HOL.
  • How do programmers use unsafe rust?
    Item type: Conference Paper
    Astrauskas, Vytautas; Matheja, Christoph; Poli, Federico; et al. (2020)
    Proceedings of the ACM on Programming Languages
    Rust’s ownership type system enforces a strict discipline on how memory locations are accessed and shared. This discipline allows the compiler to statically prevent memory errors, data races, inadvertent side effects through aliasing, and other errors that frequently occur in conventional imperative programs. However, the restrictions imposed by Rust’s type system make it difficult or impossible to implement certain designs, such as data structures that require aliasing (e.g. doubly-linked lists and shared caches). To work around this limitation, Rust allows code blocks to be declared as unsafe and thereby exempted from certain restrictions of the type system, for instance, to manipulate C-style raw pointers. Ensuring the safety of unsafe code is the responsibility of the programmer. However, an important assumption of the Rust language, which we dub the Rust hypothesis, is that programmers use Rust by following three main principles: use unsafe code sparingly, make it easy to review, and hide it behind a safe abstraction such that client code can be written in safe Rust. Understanding how Rust programmers use unsafe code and, in particular, whether the Rust hypothesis holds is essential for Rust developers and testers, language and library designers, as well as tool developers. This paper studies empirically how unsafe code is used in practice by analysing a large corpus of Rust projects to assess the validity of the Rust hypothesis and to classify the purpose of unsafe code. We identify queries that can be answered by automatically inspecting the program’s source code, its intermediate representation MIR, as well as type information provided by the Rust compiler; we complement the results by manual code inspection. Our study supports the Rust hypothesis partially: While most unsafe code is simple and well-encapsulated, unsafe features are used extensively, especially for interoperability with other languages.
  • PRIMA: General and precise neural network certification via scalable convex hull approximations
    Item type: Conference Paper
    Müller, Mark Niklas; Makarchuk, Gleb; Singh, Gagandeep; et al. (2022)
    Proceedings of the ACM on Programming Languages
    Formal verification of neural networks is critical for their safe adoption in real-world applications. However, designing a precise and scalable verifier which can handle different activation functions, realistic network architectures and relevant specifications remains an open and difficult challenge. In this paper, we take a major step forward in addressing this challenge and present a new verification framework, called PRIMA. PRIMA is both (i) general: it handles any non-linear activation function, and (ii) precise: it computes precise convex abstractions involving multiple neurons via novel convex hull approximation algorithms that leverage concepts from computational geometry. The algorithms have polynomial complexity, yield fewer constraints, and minimize precision loss. We evaluate the effectiveness of PRIMA on a variety of challenging tasks from prior work. Our results show that PRIMA is significantly more precise than the state-of-the-art, verifying robustness to input perturbations for up to 20%, 30%, and 34% more images than existing work on ReLU-, Sigmoid-, and Tanh-based networks, respectively. Further, PRIMA enables, for the first time, the precise verification of a realistic neural network for autonomous driving within a few minutes.
  • Deductive Verification with Ghost Monitors
    Item type: Conference Paper
    Clochard, Martin; Marché, Claude; Paskevich, Andrei (2020)
    Proceedings of the ACM on Programming Languages
    We present a new approach to deductive program verification based on auxiliary programs called ghost monitors. This technique is useful when the syntactic structure of the target program is not well suited for verification, for example, when an essentially recursive algorithm is implemented in an iterative fashion. Our approach consists in implementing, specifying, and verifying an auxiliary program that monitors the execution of the target program, in such a way that the correctness of the monitor entails the correctness of the target. The ghost monitor maintains the necessary data and invariants to facilitate the proof. It can be implemented and verified in any suitable framework, which does not have to be related to the language of the target programs. This technique is also applicable when we want to establish relational properties between two target programs written in different languages and having different syntactic structure. We then show how ghost monitors can be used to specify and prove fine-grained properties about the infinite behaviors of target programs. Since this cannot be easily done using existing verification frameworks, we introduce a dedicated language for ghost monitors, with an original construction to catch and handle divergent executions. The soundness of the underlying program logic is established using a particular flavor of transfinite games. This language and its soundness are formalized and mechanically checked.
  • Relaxing Alias Analysis: Exploring the Unexplored Space
    Item type: Journal Article
    Weber, Michel; Theodoridis, Theodoros; Su, Zhendong (2025)
    Proceedings of the ACM on Programming Languages
    Alias analysis is a fundamental compiler analysis that powers numerous optimizations. While research has focused on deriving more precise alias information assuming that the compiler will optimize better, recent work shows a negligible, or even negative, performance impact of alias information. In this work, we shift the perspective from refining to relaxing alias information, i.e., removing information, to complement existing work and challenge that assumption systematically. Our study on a state-of-the-art compiler, LLVM, running the SPEC CPU 2017 benchmark suite, shows (1) a small overall impact - removing alias analysis entirely has little impact on the final binaries, (2) few influential queries - only a small fraction, namely ĝ1/43%, of the alias information leads to changes in the final binary, and (3) lost potential - random relaxations can reduce execution time by 21% and binary size by 39% for certain cases, suggesting that compilers could better utilize alias information. Through this work, we advocate that it is beneficial for future research to avoid simply refining the general precision of alias analysis, but also to explore how to find and refine the most relevant queries, and how to more effectively utilize alias information.
  • Generative type-aware mutation for testing SMT solvers
    Item type: Conference Paper
    Park, Jiwon; Winterer, Dominik; Zhang, Chengyu; et al. (2021)
    Proceedings of the ACM on Programming Languages
    We propose Generative Type-Aware Mutation, an effective approach for testing SMT solvers. The key idea is to realize generation through the mutation of expressions rooted with parametric operators from the SMT-LIB specification. Generative Type-Aware Mutation is a hybrid of mutation-based and grammar-based fuzzing and features an infinite mutation space—overcoming a major limitation of OpFuzz, the state-of-the-art fuzzer for SMT solvers. We have realized Generative Type-Aware Mutation in a practical SMT solver bug hunting tool, TypeFuzz. During our testing period with TypeFuzz, we reported over 237 bugs in the state-of-the-art SMT solvers Z3 and CVC4. Among these, 189 bugs were confirmed and 176 bugs were fixed. Most notably, we found 18 soundness bugs in CVC4’s default mode alone. Several of them were two years latent (7/18). CVC4 has been proved to be a very stable SMT solver and has resisted several fuzzing campaigns.
  • SMT2Test: From SMT Formulas to Effective Test Cases
    Item type: Journal Article
    Zhang, Chengyu; Su, Zhendong (2024)
    Proceedings of the ACM on Programming Languages
    One of the primary challenges in software testing is generating high-quality test inputs and obtaining corresponding test oracles. This paper introduces a novel methodology to mitigate this challenge in testing program verifiers by employing SMT (Satisfiability Modulo Theories) formulas as a universal test case generator. The key idea is to transform SMT formulas into programs and link the satisfiability of the formulas with the safety property of the programs, allowing the satisfiability of the formulas to act as a test oracle for program verifiers. This method was implemented as a framework named SMT2Test, which enables the transformation of SMT formulas into Dafny and C programs. An intermediate representation was designed to augment the flexibility of this framework, streamlining the transformation for other programming languages and fostering modular transformation strategies. We evaluated the effectiveness of SMT2Test by finding defects in two program verifiers: the Dafny verifier and CPAchecker. Utilizing the SMT2Test framework with the SMT formulas from the SMT competition and SMT solver fuzzers, we discovered and reported a total of 14 previously unknown defects in these program verifiers that were not found by previous methods. After reporting, all of them have been confirmed, and 6 defects have been fixed. These findings show the effectiveness of our method and imply its potential application in testing other programming language infrastructures.
  • Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks
    Item type: Journal Article
    Müller, Mark Niklas; Fischer, Marc; Staab, Robin; et al. (2023)
    Proceedings of the ACM on Programming Languages
    We present a new abstract interpretation framework for the precise over-approximation of numerical fixpoint iterators. Our key observation is that unlike in standard abstract interpretation (AI), typically used to over-approximate all reachable program states, in this setting, one only needs to abstract the concrete fixpoints, i.e., the final program states. Our framework targets numerical fixpoint iterators with convergence and uniqueness guarantees in the concrete and is based on two major technical contributions: (i) theoretical insights which allow us to compute sound and precise fixpoint abstractions without using joins, and (ii) a new abstract domain, CH-Zonotope, which admits efficient propagation and inclusion checks while retaining high precision. We implement our framework in a tool called CRAFT and evaluate it on a novel fixpoint-based neural network architecture (monDEQ) that is particularly challenging to verify. Our extensive evaluation demonstrates that CRAFT exceeds the state-of-the-art performance in terms of speed (two orders of magnitude), scalability (one order of magnitude), and precision (25% higher certified accuracies).
  • Miri: Practical Undefined Behavior Detection for Rust
    Item type: Journal Article
    Jung, Ralf; Kimock, Benjamin; Poveda, Christian; et al. (2026)
    Proceedings of the ACM on Programming Languages
    The Rust programming language has two faces: on the one hand, it is a high-level language with a strong type system ensuring memory and thread safety. On the other hand, Rust crucially relies on unsafe code for cases where the compiler is unable to statically ensure basic safety properties. The challenges of writing unsafe Rust are similar to those of writing C or C++: a single mistake in the program can lead to Undefined Behavior, which means the program is no longer described by the language's Abstract Machine and can go wrong in arbitrary ways, often causing security issues. Ensuring the absence of Undefined Behavior bugs is therefore a high priority for unsafe Rust authors. In this paper we present Miri, the first tool that can find all de-facto Undefined Behavior in deterministic Rust programs. Some of the key non-trivial features of Miri include tracking of pointer provenance, validation of Rust type invariants, data-race detection, exploration of weak memory behaviors, and implementing enough basic OS APIs (such as file system access and concurrency primitives) to be able to run unchanged real-world Rust code. In an evaluation on more than 100 000 Rust libraries, Miri was able to successfully execute more than 70% of the tests across their combined test suites. Miri has found dozens of real-world bugs and has been integrated into the continuous integration of the Rust standard library and many prominent Rust libraries, preventing many more bugs from ever entering these codebases.
Publications1 - 10 of 78