7,482 papers · page 31 of 375
Modern Integrated Development Environments (IDEs) offer automated refactorings to aid programmers in developing and maintaining software. However, implementing sound automated refactorings is challenging, as refactorings may inadvertently introduce name-binding errors or cause re…
Computing derivatives is paramount for multiple domains ranging from training neural networks to precise climate simulations. While derivatives can be generated by Automatic Differentiation (AD) tools, they often require aggressive optimization to avoid compromising program perfo…
Many imperative programming languages offer global variables to implement common functionality such as global caches and counters. Global variables are typically initialized by module initializers (e.g., static initializers in Java), code blocks that are executed automatically by…
Accessing an arbitrary element of a singly linked list or cons list requires traversing up to a linear number of pointers. The applicative random-access list is a data structure that behaves like a cons list except that accessing an arbitrary element traverses only a logarithmic …
Resource analysis aims to derive symbolic resource bounds of programs. Although numerous resource-analysis techniques have been developed—ranging from static to dynamic and manual to automated techniques—they each come with their own distinct strengths and weaknesses. To overcome…
Clients rely on database systems to be correct, which requires the system not only to implement transactions’ semantics correctly but also to provide isolation guarantees for the transactions. This paper presents a client-centric technique for checking both semantic correctness a…
The selection monad on a set consists of selection functions. These select an element from the set, based on a loss (dually, reward) function giving the loss resulting from a choice of an element. Abadi and Plotkin used the monad to model a language with operations making choices…
Actors are lightweight reactive processes that communicate by asynchronous message-passing. Actors address common problems like concurrency control and fault tolerance, but resource management remains challenging: in all four of the most popular actor frameworks (Pekko, Akka, Erl…
The past few years have seen a surge of interest in choreographic programming, a programming paradigm for concurrent and distributed systems. The paradigm allows programmers to implement a distributed interaction protocol with a single high-level program, called a choreography, a…
Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In …
The C and C++ languages define hundreds of cases as having undefined behavior (UB). These include, for example, corner cases where different CPU architectures disagree on the semantics of an instruction and the language does not want to force a specific implementation (e.g., shif…
Live programming environments provide various semantic services, including type checking and evaluation, continuously as the user is editing the program. The live paradigm promises to improve the developer experience, but liveness is an implementation challenge, particularly when…
Structure editors operate directly on a program’s syntactic tree structure. At first glance, this allows for the exciting possibility that such an editor could enforce correctness properties: programs could be well-formed and sometimes even well-typed by construction. Unfortunate…
Large-scale, revenue-critical application services are often written in Java or other memory-safe languages whose type systems do not expose immutable state. Such applications are especially exposed to garbage collection performance overheads because latency, throughput, and memo…
Blockchains operating at the global scale demand high-performance byzantine fault-tolerant (BFT) consensus protocols. Most classic PBFT-like protocols suffer from an issue known as the leader bottleneck, which severely limits their throughput and resource utilization. Recently, D…
We define webs to be the collections of producers and consumers (e.g., functions and calls) in a program that are constrained: in higher-order languages, multiple functions can flow to the same call, all of which must agree on an interface (e.g., calling convention). We argue tha…
Regression testing is an essential part of software development, but it suffers from the presence of flaky tests - tests that pass and fail non-deterministically when run on the same code. These unpredictable failures waste developers’ time and often hide real bugs. Prior work sh…
Software updates, including bug repair and feature additions, are frequent in modern applications but they often leave test suites outdated, resulting in undetected bugs and increased chances of system failures. A recent study by Meta revealed that 14%-22% of software failures st…
Heisenbugs, notorious for their ability to change behavior and elude reproducibility under observation, are among the toughest challenges in debugging programs. They often evade static detection tools, making them especially prevalent in cyber-physical edge systems characterized …
Mechanisations of programming language specifications are now increasingly common, providing machine-checked modelling of the specification and verification of desired properties such as type safety. However it is challenging to maintain these mechanisations, particularly in the …