7,482 papers · page 5 of 375
Samantha Frohlich, Jessica Foster, G. A. Kavvos, Meng Wang
Representing bound variables in embedded languages is a challenging problem, often requiring painful tradeoffs between expressivity and usability. On the one hand, first-order representations using de Bruijn indices have many nice properties, but quickly become difficult to read …
Elisa Fröhlich, Angelica Aparecida Moreira, Fernando Magno Quintão Pereira
Profile-guided optimization (PGO) is a well-established technique for improving program performance, being integrated into major compilers such as GCC, LLVM/Clang, and Microsoft Visual C++. PGO collects information about a program’s execution and uses it to guide optimizations su…
Aymeric Fromherz, Jonathan Protzenko
The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C. Automatically translating C to Rust is thus an appealing course of action. Several works have gone down this path, handling an ever-increasing subset of C through a variet…
Ryan Thomas Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, Anil Madhavapeddy
Package managers are legion. Every programming language and operating system has its own solution, each with subtly different semantics for dependency resolution. This fragmentation prevents multilingual projects from expressing precise dependencies across language ecosystems; it…
Andrea Gilot, Tobias Wrigstad, Eva Darulova
Reasoning about floating-point arithmetic is notoriously hard. While static and dynamic analysis techniques or program repair have made significant progress, more work is still needed to make them relevant to real-world code. On the critical path to that goal is understanding wha…
Giulia Giusti, Michele Pagani
JAX Autodiff refers to the core of the automatic differentiation (AD) systems developed in projects like JAX and Dex. JAX Autodiff has recently been formalised in a linear typed calculus by Radul et al in POPL 2023. Although this formalisation suffices to express the main program…
Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey
Multi-modal program verification is a process of validating code against its specification using both dynamic and symbolic techniques, and proving its correctness by a combination of automated and interactive machine-assisted tools. In order to be trustworthy, such verification t…
Amir Kafshdar Goharshady, Kerim Kochekov, Tian Shu, Ahmed Khaled Zaher
Binary size reduction is an increasingly important optimization objective for compilers, especially in the context of mobile applications and resource-constrained embedded devices. In such domains, binary size often takes precedence over compilation time. One emerging technique t…
Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, Benjamin C. Pierce
Among the biggest challenges in property-based testing (PBT) is the constrained random generation problem : given a predicate on program values, randomly sample from the set of all values, and only values, satisfying that predicate. Efficient solutions to this problem are critica…
Shaurya Gomber, Debangshu Banerjee, Gagandeep Singh
Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, giving rise to three significant limitations. First, extensibility is limited because transformers cannot be reused across domains and new transform…
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, Stefano Volpe
The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotati…
Trayan Gospodinov, Peter Müller, Thibault Dardinier
Many important functional and security properties—including non-interference, determinism, and generalized non-interference (GNI)—are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes…
Hemant Gouni, Frank Pfenning, Jonathan Aldrich
Substructural type systems provide the ability to speak about resources. By enforcing usage restrictions on inputs to computations they allow programmers to reify limited system units—such as memory—in types. We demonstrate a new form of resource reasoning founded on constraining…
Harrison Grodin, Runming Li, Robert Harper
Software development depends on the use of libraries whose public specifications inform client code and impose obligations on private implementations; it follows that verification at scale must also be modular, preserving such abstraction. Hoare's influential methodology uses abs…
Jan Grünke, Thomas Haas, Roland Meyer
We present a model checking approach for axiomatic memory consistency models written in the language CAT. It can prove properties of single memory models like the monotonicity of barriers, and also compare models like TSO and ARM8. To achieve this expressiveness, our approach sup…
Qiuhan Gu, Avaljot Singh, Gagandeep Singh
How to construct globally sound abstract interpreters to safely approximate program behaviors remains a bottleneck in abstract interpretation. In this paper, we show the potential of using state-of-the-art LLMs to automate this tedious process. Focusing on the neural network veri…
Kevin Guan, Pengyue Jiang, Milos Gligoric, Owolabi Legunsen
Inline tests validate single program statements and were shown to find single-statement bugs or kill mutants that unit tests miss. Inline tests complement unit tests by enabling testing at a finer program granularity level than methods. So, inline tests can more easily find fault…
Zhichao Guan, Tailai Yu, Di Wang, Zhenjiang Hu
Syntactic sugar enhances the usability of a core language by providing intuitive syntax in a surface language; however, its interaction with the core-language type checker often results in error messages that are unclear to surface programmers. Existing techniques, such as type l…
Yujiang Gui, Yonggang Tao, Jingling Xue
Taint analysis, widely used for bug and vulnerability detection, is typically formulated as a flow- and context-sensitive IFDS analysis. To achieve field sensitivity, IFDS models heap locations as k -limited access paths but suffers from cubic time and quadratic space complexity,…
Tobias Gürtler, Benjamin Lucien Kaminski
Probabilistic programming languages (PPLs) are an expressive and intuitive means of representing complex probability distributions. In that realm, languages like Dice target an important class of probabilistic programs: those whose probability distributions are discrete. Discrete…