1,205 papers · page 20 of 61
Pointer analysis benefits many useful clients, such as compiler optimizations and bug finding tools. Unfortunately, common programming language features such as dynamic loading, reflection, and foreign language interfaces, make pointer analysis difficult. This article describes h…
The π-calculus, a calculus of mobile processes, can compositionally represent dynamics of major programming constructs by decomposing them into name passing. The present work reports our experience in using a linear/affine typed π-calculus for the analysis and development of type…
Interprocedural data flow analysis extends the scope of analysis across procedure boundaries in search of increased optimization opportunities. Call strings based approach is a general approach for performing flow and context sensitive interprocedural analysis. It maintains a his…
Despite significant progress in the theory and practice of program analysis, analyzing properties of heap data has not reached the same level of maturity as the analysis of static and stack data. The spatial and temporal structure of stack and static data is well understood while…
Modern JVM implementations interleave execution with compilation of “hot” methods to achieve reasonable performance. Since compilation overhead impacts the execution time of the application and induces run-time pauses, we explore offloading compilation onto a compilation server. …
With the diverging improvements in CPU speeds and memory access latencies, detecting and removing memory access bottlenecks becomes increasingly important. In this work we present METRIC, a software framework for isolating and understanding such bottlenecks using partial access t…
A Changing of the GuardSince 1979, the ACM Transactions on Programming Languages and Systems (TOPLAS) has been the premier journal for the publication of research papers in the area of programming languages and systems to assist the task of programming.There are many reasons for …
XSL Transformations (XSLT) is a programming language for defining transformations among XML languages. The structure of these languages is formally described by schemas, for example using DTD or XML Schema, which allows individual documents to be validated. However, existing XSLT…
We consider integer arithmetic modulo a power of 2 as provided by mainstream programming languages like Java or standard implementations of C. The difficulty here is that, for w > 1, the ring Z m of integers modulo m = 2 w has zero divisors and thus cannot be embedded into a fiel…
This article develops a proof theory for low-level code languages. We first define a proof system, which we refer to as the sequential sequent calculus , and show that it enjoys the cut elimination property and that its expressive power is the same as that of the natural deductio…
A reference-counting garbage collector cannot reclaim unreachable cyclic structures of objects. Therefore, reference-counting collectors either use a backup tracing collector infrequently, or employ a cycle collector to reclaim cyclic structures. We propose a new concurrent cycle…
The subject of this article is flow- and context-insensitive pointer analysis. We present a novel approach for precisely modelling struct variables and indirect function calls. Our method emphasises efficiency and simplicity and is based on a simple language of set constraints. W…
The notion of control dependence underlies many program analysis and transformation techniques. Despite being widely used, existing definitions and approaches to calculating control dependence are difficult to apply directly to modern program structures because these make substan…
In order to achieve better precision of abstract interpretation-based static analysis, we introduce a new generic abstract domain, the trace partitioning abstract domain. We develop a theoretical framework allowing a wide range of instantiations of the domain, proving that all th…
No abstract available.
One proposal for automatic construction of proofs about programs is to combine Hoare logic and abstract interpretation. Constructing proofs is in Hoare logic. Discovering programs' invariants is done by abstract interpreters. One problem of this approach is that abstract interpre…
We study HMG(X), an extension of the constraint-based type system HM(X) with deep pattern matching, polymorphic recursion, andguarded algebraic data types. Guarded algebraic data types subsume the concepts known in the literature asindexed types,guarded recursive datatype constru…
This article presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program's type structure to change dynamically but guarantees the updated program remains type-correct by en…
Existing algorithms for computing dominators are formulated for control flow graphs of single procedures. With the rise of computing power, and the viability of whole-program analyses and optimizations, there is a growing need to extend the dominator computation algorithms to con…