1,205 papers · page 18 of 61
Foreign function interfaces (FFIs) allow components in different languages to communicate directly with each other. While FFIs are useful, they often require writing tricky low-level code and include little or no static safety checking, thus providing a rich source of hard-to-fin…
Java Virtual Machines (JVMs) traditionally perform bytecode verification by way of an iterative dataflow analysis. Bytecode verification is necessary to ensure type safety because temporary variables in the JVM are not statically typed. We present an alternative verification mech…
Object layout schemes used in C++ and other languages rely on (sometimes numerous) compiler generated fields. We describe a language-independent object layout scheme, which is space optimal, that is, objects are contiguous, and contain no compiler generated fields other than a si…
Reasoning about multithreaded object-oriented programs is difficult, due to the nonlocal nature of object aliasing and data races. We propose a programming regime (or programming model ) that rules out data races, and enables local reasoning in the presence of object aliasing and…
In this article we present Jedd, a language extension to Java that supports a convenient way of programming with Binary Decision Diagrams (BDDs). The Jedd language abstracts BDDs as database-style relations and operations on relations, and provides static type rules to ensure tha…
In the context of statically typed, class-based languages , we investigate classes that can be extended with trait composition. A trait is a collection of methods without state; it can be viewed as an incomplete stateless class . Traits can be composed in any order, but only make…
Current critical systems often use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky,…
Nondeterminacy is a fundamental notion in computing. We show that it can be described by a general theory that accounts for it in the form in which it occurs in many programming contexts, among them specifications, competing agents, data refinement, abstract interpretation, imper…
Type systems and model checking are two prevalent approaches to program verification. A prominent difference between them is that type systems are typically defined in a syntactic and modular style whereas model checking is usually performed in a semantic and whole-program style.…
Compile-time optimizations generally improve program performance. Nevertheless, degradations caused by individual compiler optimization techniques are to be expected. Feedback-directed optimization orchestration systems generate optimized code versions under a series of optimizat…
As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages which treat probability distributions as primitive datatypes. Most probabilistic languages, however, focus only on discrete distributions and have …
We show that reverse-mode AD (Automatic Differentiation)—a generalized gradient-calculation operator—can be incorporated as a first-class function in an augmented lambda calculus, and therefore into a functional-programming language. Closure is achieved, in that the new operator …
Malware detection is a crucial aspect of software security. Current malware detectors work by checking for signatures , which attempt to capture the syntactic characteristics of the machine-level byte sequence of the malware. This reliance on a syntactic approach makes current de…
We introduce the notion of apartially-flow-sensitive analysis based on the number of read and write operations that are guaranteed to be analyzed in a sequential manner. We study the complexity of partially-flow-sensitive alias analysis and show that precise alias analysis with a…
This article investigates register allocation for software pipelined multidimensional loops where the execution of successive iterations from an n -dimensional loop is overlapped. For single loop software pipelining, the lifetimes of a loop variable in successive iterations of th…
This article presents a model and implementation techniques for speeding up constraint propagation. Three fundamental approaches to improving constraint propagation based on propagators as implementations of constraints are explored: keeping track of which propagators are at fixp…
We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with “witnesses,” which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctn…
This article presents a static system for checking determinism (technically, partial confluence) of communicating concurrent processes. Our approach automatically detects partial confluence in programs communicating via a mix of different kinds of communication methods: rendezvou…
We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logics to formally spec…
Domain specific languages (DSLs) are mini-languages that are increasingly seen as being a valuable tool for software developers and non-developers alike. DSLs must currently be created in an ad-hoc fashion, often leading to high development costs and implementations of variable q…