Programming Languages and Systems (TOPLAS)


Search Issue
enter search term and/or author name


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 15 Issue 1, Jan. 1993

The derivation of distributed termination detection algorithms from garbage collection schemes
Gerard Tel, Friedemann Mattern
Pages: 1-35
DOI: 10.1145/151646.151647
It is shown that the termination detection problem for distributed computations can be modeled as an instance of the garbage collection problem. Consequently, algorithms for the termination detection problem are obtained by applying...

The concurrency workbench: a semantics-based tool for the verification of concurrent systems
Rance Cleaveland, Joachim Parrow, Bernhard Steffen
Pages: 36-72
DOI: 10.1145/151646.151648
The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: a variety of different verification methods, including...

Composing specifications
Martín Abadi, Leslie Lamport
Pages: 73-132
DOI: 10.1145/151646.151649
A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle because a component need behave...

A general framework for semantics-based bottom-up abstract interpretation of logic programs
Roberto Barbuti, Roberto Giacobazzi, Giorgio Levi
Pages: 133-181
DOI: 10.1145/151646.151650
The theory of abstract interpretation provides a formal framework to develop advanced dataflow analysis tools. The idea is to define a nonstandard semantics which is able to compute, in finite time, an approximated model of the program. In this...

Lazy caching
Yehuda Afek, Geoffrey Brown, Michael Merritt
Pages: 182-205
DOI: 10.1145/151646.151651
This paper examines cache consistency conditions for multiprocessor shared memory systems. It states and motivates a weaker condition than is normally implemented. An algorithm is presented that exploits the weaker condition to achieve greater...

Technical correspondence: a correction to the denotational semantics for the Prolog of Nicholson and Foo
Alan Finlay, Lloyd Allison
Pages: 206-208
DOI: 10.1145/151646.151652