7,482 papers · page 33 of 375
We present a general form of temporal effects for recursive types. Temporal effects have been adopted by effect systems to verify both linear-time temporal safety and liveness properties of higher-order programs with recursive functions. A challenge in a generalization to recursi…
Many quantum algorithms instantiate and use ancillas, spare qubits that serve as temporary storage in a quantum circuit. In particular, many recently developed high-level and modular quantum programming languages (QPLs) use ancilla qubits to implement various programming construc…
Software systems change on a continuous basis, with each patch prone to int roducing new errors and security vulnerabilities. While providing a full functional specification for the program is a notoriously difficult task, writing a patch specification that describes the behaviou…
Context-free language (CFL) reachability is a critical framework for various program analyses, widely adopted despite its computational challenges due to cubic or near-cubic time complexity. This often leads to significant performance degradation in client applications. Notably, …
Interactive theorem provers, or proof assistants, are important tools across many areas of computer science and mathematics, but even experts find them challenging to use effectively. To improve their design, we need a deeper, user-centric understanding of proof assistant usage. …
Bayesian program analysis is a systematic approach to learn from external information for better accuracy by converting logical deduction in conventional program analysis into Bayesian inference. A key challenge in Bayesian program analysis is how to select program abstractions t…
The R programming language is primarily designed for statistical computing and mostly used by researchers without a background in computer science. R provides a wide range of dynamic features and peculiarities that are difficult to analyze statically like dynamic scoping and lazy…
The uninterpretability of Deep Neural Networks (DNNs) hinders their use in safety-critical applications. Abstract Interpretation-based DNN certifiers provide promising avenues for building trust in DNNs. Unsoundness in the mathematical logic of these certifiers can lead to incorr…
In this paper we demonstrate a technique for developing high performance applications with strong correctness guarantees. Using a theorem prover, we derive a high-level specification of the application that includes correctness invariants of our choice. After that, within the sam…
We present PRISM, a novel technique for detecting overfitting patches in automatic program repair (APR). Despite significant advances in APR, overfitting patches—those passing test suites but not fixing bugs—persist, degrading performance and increasing developer review burden. T…
Although existing garbage collectors (GCs) perform extremely well on typical programs, there still exist pathological programs for which modern GCs significantly degrade performance. This observation begs the question: might there exist a ‘holy grail’ GC algorithm, as yet undisco…
Data replication is crucial for enabling fault tolerance and uniform low latency in modern decentralized applications. Replicated Data Types (RDTs) have emerged as a principled approach for developing replicated implementations of basic data structures such as counter, flag, set,…
The separation logic framework Iris has been built on the premise that all assertions are stable, meaning they unconditionally enjoy the famous frame rule. This gives Iris—and the numerous program logics that build on it—very modular reasoning principles. But stability also comes…
Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these…
Static analysis of real-world programs combines flow- and context-sensitive analyses of local program states with computation of flow- and context-insensitive invariants at globals, that, e.g., abstract data shared by multiple threads. The values of locals and globals may mutuall…
There are many different probabilistic programming languages that are specialized to specific kinds of probabilistic programs. From a usability and scalability perspective, this is undesirable: today, probabilistic programmers are forced up-front to decide which language they wan…
The ways in which the components of a program interact with each other in a concurrent setting can be considerably more complex than in a sequential setting. The core problem is unrestricted shared mutable state. An alternative to unrestricted shared mutable state is to restrict …
Satisfiability Modulo Theories (SMT) solvers are widely used for program analysis and other applications that require automated reasoning. Rewrite systems, as crucial integral components of SMT solvers, are responsible for simplifying and transforming formulas to optimize the sol…
MLIR (Multi-Level Intermediate Representation) compiler infrastructure provides an efficient framework for introducing a new abstraction level for programming languages and domain-specific languages. It has attracted widespread attention in recent years and has been applied in va…
An open program is one for which the complete source code is not available, which is a reality for real-world program verification. Software verification tools tend to assume the worst about any unconstrained behavior and this can yield an enormous number of spurious warnings for…