1,205 papers · page 13 of 61
Dedicated to the memory of John C. Reynolds (1935--2013). We present Relational Hoare Type Theory (RHTT), a novel language and verification system capable of expressing and verifying rich information flow and access control policies via dependent types. We show that a number of s…
Reachability from a program variable v to a program variable w states that from v , it is possible to follow a path of memory locations that leads to the object bound to w . We present a new abstract domain for the static analysis of possible reachability between program variable…
No abstract available.
ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into mutually recursive, separately compilable components. Mixin modules facilitate recursive linking of s…
Growing interest in graphics processing units has brought renewed attention to the Single Instruction Multiple Data (SIMD) execution model. SIMD machines give application developers tremendous computational power; however, programming them is still challenging. In particular, dev…
This article presents a family of static analyses to determine pointer targets, control flow, and dataflow in combination. The integrated solution to these mutually dependent problems approaches the result from the optimistic side. It is a general strategy for static program anal…
First-class classes enable programmers to abstract over patterns in the class hierarchy and to experiment with new forms of object-oriented programming such as mixins and traits. This increase in expressive power calls for tools to control the complexity of the software architect…
We study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization or sized types bound the resource usage or result size of such a procedure by a sum of unary functions of the size…
In this article we study the decidability of termination of several variants of simple integer loops, without branching in the loop body and with affine constraints as the loop guard (and possibly a precondition). We show that termination of such loops is undecidable in some case…
Dynamic memory allocation is ubiquitous in today's runtime environments. Allocation and deallocation of objects during program execution may cause fragmentation and foil the program's ability to allocate objects. Robson [1971] has shown that a worst-case scenario can create a spa…
Finite-state properties account for an important class of program properties, typically related to the order of operations invoked on objects. Many library implementations therefore include manually written finite-state monitors to detect violations of finite-state properties at …
We propose a small-step operational semantics to support reasoning about Web applications written in the multitier language HOP. The semantics covers both server side and client side computations, as well as their interactions, and includes creation of Web services, distributed c…
This article relates two different paradigms of descriptions of communication behavior, one focusing on global message flows and another on end-point behaviors, using formal calculi based on session types. The global calculus, which originates from a Web service description langu…
Concurrency-related errors, such as data races, are frustratingly difficult to track down and eliminate in large object-oriented programs. Traditional approaches to preventing data races rely on protecting instruction sequences with synchronization operations. Such control-centri…
Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol …
Aspect-oriented programming (AOP) has produced interesting language designs, but also ad hoc semantics that needs clarification. We contribute to this clarification with a calculus that models essential AOP, both simpler and more general than existing formalizations. In AOP, advi…
Asynchronous programming is a ubiquitous systems programming idiom for managing concurrent interactions with the environment. In this style, instead of waiting for time-consuming operations to complete, the programmer makes a non-blocking call to the operation and posts a callbac…
A large body of data-flow analyses exists for analyzing and optimizing sequential code. Unfortunately, much of it cannot be directly applied on parallel code, for reasons of correctness. This article presents a technique to automatically, aggressively, yet safely apply sequential…
Integrated Development Environments (IDEs) increase programmer productivity, providing rapid, interactive feedback based on the syntax and semantics of a language. Unlike conventional parsing algorithms, scannerless generalized-LR parsing supports the full set of context-free gra…
TOPLAS will have four issues per year from now on! The goal is to have each of the four issues contain 5--6 articles, instead of the previous schedule of six issues that each typically contained 3--4 articles. Historically, TOPLAS had four issues per volume from 1980 to 1992, and…