7,482 papers · page 13 of 375
Frank Schüssele, Matthias Zumkeller, Miriam Lagunes-Rochin, Dominik Klumpp
Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs. Automatic generation of small, compact c…
Manuel Serrano
The Proceedings of the ACM series presents the highest-quality research conducted in diverse areas of computer science, as represented by the ACM Special Interest Groups (SIGs). The Proceedings of the ACM on Programming Languages (PACMPL) focuses on research on all aspects of pro…
Ritvik Sharma, Cheng Peng, Siddharth Dangwal, Sara Achour
Simulation of physics problems is one of the most important use cases of quantum computing. For this class of problems, the goal is typically to find the minimum energy state, or the ground state, of a physical system’s Hamiltonian. These problems frequently have constraints, suc…
Yuanfeng Shi, Ziyue Jin, Xin Zhang
Abstract interpretation has served as a foundational framework for static program analysis, enabling the over approximation of program semantics to be sound (i.e., no false negatives) but often at the cost of false alarms due to incompleteness. Although prior efforts to address f…
Chenghang Shi, Haofeng Li, Jie Lu, Lian Li
Context-free language (CFL) reachability is a fundamental framework widely used to model a variety of program analysis tasks, though it often suffers from inherent inefficiency due to its (sub)cubic time complexity. In this paper, we propose a novel perspective, relation chaining…
Zheng Shi, Lasse Møldrup, Umang Mathur, Andreas Pavlogiannis
A key computational question underpinning the automated testing and verification of concurrent programs is the consistency question — given a partial execution history, can it be completed in a consistent manner? Due to its importance, consistency testing has been studied extensi…
Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao, Spencer Wang, Gus Henry Smith + 2 more
During chip development, engineers must target different technologies, such as simulation and various ASIC and FPGA technologies. Conventionally, they split parts of the code (e.g., memories) into separate technology-specialized blocks implementing the same high-level behavior. T…
Thodoris Sotiropoulos, Zhendong Su
We propose error enumeration , a method that aims to discover soundness defects in type analyzers by generating ill-typed programs by construction. Given a well-typed program 𝑃 , it systematically injects type mismatches at all possible program locations to explore ill-typed prog…
David Spielmann, George Zakhour, Dominik Arnold, Matteo Biagiola, Roland Meier, Guido Salvaneschi
Infrastructure-as-Code (IaC) engines, such as Terraform, OpenTofu, and Pulumi, automate the provisioning and management of cloud resources. They parse IaC specifications and orchestrate the required actions, making them the backbone of modern clouds, and critical to the reliabili…
Manu Sridharan
The Proceedings of the ACM series presents the highest-quality research conducted in diverse areas of computer science, as represented by the ACM Special Interest Groups (SIGs). The Proceedings of the ACM on Programming Languages (PACMPL) focuses on research on all aspects of pro…
Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, Michael Garland
Data races, which occur when two or more threads incorrectly access the same memory location without appropriate synchronization, cause CUDA programmers considerable pain. Even experts struggle to reason about extreme parallelism, multiple memory spaces and scopes, and diverse sy…
J. Ryan Stinnett, Stephen Kell
Debugging tools rely on compiler-generated metadata to present a source-language view, but current compilers often throw away or corrupt debugging information in optimised programs. Attempts to test debugging information are confounded by ad-hoc limitations of the debug info form…
Fridtjof Peer Stoldt, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Tobias Wrigstad
Immutability is common in the programming mainstream: deep immutability is the default in functional languages while imperative languages typically provide opt-in support for shallow immutability, usually enforced through static checking. Python is a dynamic imperative language w…
Bonan Su, Yuan Feng, Mingsheng Ying, Li Zhou
In this paper, we define an assertion language designed for expectation-based reasoning about quantum programs. The key design idea is a representation of quantum predicates by quasi-probability distributions of generalized Pauli operators. Then we extend classical techniques suc…
Wenhao Tang, Sam Lindley
Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in …
Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert
Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular a…
Matthew Toohey, Yanning Chen, Ara Jamalzadeh, Ningning Xie
This paper proposes a novel language design that combines extensible data types, implemented through row types and row polymorphism, with ad-hoc polymorphism, implemented through type classes. Our design introduces several new constructs and constraints useful for generic operati…
Hünkar Can Tunç, Yifan Dong, Andreas Pavlogiannis
Atomicity is a fundamental abstraction in concurrency, specifying that program behavior can be understood by considering specific code blocks executing atomically. However, atomicity invariants are tricky to maintain while also optimizing for code efficiency, and atomicity violat…
April Tune, G. A. Kavvos
We develop a compositional semantics for abstract machines, focusing on CK/CEK machines for call-by-push-value. Taking abstract machines as the primary operational semantics, we introduce bimodels, which give denotations to both programs and stacks, and environment bimodels, whic…
Abhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza, P. Madhusudan, Adithya Murali
We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the library methods used by the client that are…