7,482 papers · page 13 of 375
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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 …
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…
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…
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…
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…
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…