Programming Languages and Systems (TOPLAS)


Search Issue
enter search term and/or author name


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 16 Issue 5, Sept. 1994

Efficiently counting program events with support for on-line queries
Thomas Ball
Pages: 1399-1410
DOI: 10.1145/186025.186027
The ability to count events in a program's execution is required by many program analysis applications. We represent an instrumentation method for efficiently counting events in a program's execution, with support for on-line queries of the...

Polymorphic type inference and abstract data types
Konstantin Läufer, Martin Odersky
Pages: 1411-1430
DOI: 10.1145/186025.186031
Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be...

Fixpoint computation for polyvariant static analyses of higher-order applicative programs
J. Michael Ashley, Charles Consel
Pages: 1431-1448
DOI: 10.1145/186025.186037
This paper presents an optimized general-purpose algorithm for polyvariant, static analyses of higher-order applicative programs. A polyvariant analysis is a very accurate form of analysis that produces many more abstract descriptions for a...

Strictness optimization for graph reduction machines (why id might not be strict)
Marcel Beemster
Pages: 1449-1466
DOI: 10.1145/186025.186040
Strictness optimizations in the implementation of lazy functional languages are not always valid. In nonoptimized graph reduction, evaluation always takes place at the request of case analysis or a primitive operation. Hence, the result of a...

The undecidability of aliasing
G. Ramalingam
Pages: 1467-1471
DOI: 10.1145/186025.186041
Alias analysis is a prerequisite for performing most of the common program analyses such as reaching-definitions analysis or live-variables analysis. Landi [1992] recently established that it is impossible to compute statically precise alias...

A generalized theory of bit vector data flow analysis
Uday P. Khedker, Dhananjay M. Dhamdhere
Pages: 1472-1511
DOI: 10.1145/186025.186043
The classical theory of data flow analysis, which has its roots in unidirectional flows, is inadequate to characterize bidirectional data flow problems. We present a generalized theory of bit vector data flow analysis which explains the known...

Model checking and abstraction
Edmund M. Clarke, Orna Grumberg, David E. Long
Pages: 1512-1542
DOI: 10.1145/186025.186051
We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the...

An old-fashioned recipe for real time
Martín Abadi, Leslie Lamport
Pages: 1543-1571
DOI: 10.1145/186025.186058
Traditional methods for specifying and reasoning about concurrent systems work for real-time systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a queue and of a mutual-exclusion protocol. In...

Extending attribute grammars to support programming-in-the-large
Josephine Micallef, Gail E. Kaiser
Pages: 1572-1612
DOI: 10.1145/186025.186091
Attribute grammars add specification of static semantic properties to context-free grammars, which, in turn, describe the syntactic structure of program units. However, context-free grammars cannot express programming-in-the-large features...

Decompilation: the enumeration of types and grammars
Peter T. Breuer, Jonathan P. Bowen
Pages: 1613-1647
DOI: 10.1145/186025.186093
While a compiler produces low-level object code from high-level source code, a decompiler produces high-level code from low-level code and has applications in the testing and validation of safety-critical software. The decompilation of an object...

Automatic isolation of compiler errors
David B. Whalley
Pages: 1648-1659
DOI: 10.1145/186025.186103
This paper describes a tool called vpoiso that was developed to isolate errors automatically in the vpo compiler system. The two general types of compiler errors isolated by this tool are optimization and...