ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 31 Issue 1, December 2008

A programming model for concurrent object-oriented programs
Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte
Article No.: 1
DOI: 10.1145/1452044.1452045

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...

Efficient constraint propagation engines
Christian Schulte, Peter J. Stuckey
Article No.: 2
DOI: 10.1145/1452044.1452046

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...

Decomposing bytecode verification by abstract interpretation
C. Bernardeschi, N. De Francesco, G. Lettieri, L. Martini, P. Masci
Article No.: 3
DOI: 10.1145/1452044.1452047

Bytecode verification is a key point in the security chain of the Java platform. This feature is only optional in many embedded devices since the memory requirements of the verification process are too high. In this article we propose an approach...

A probabilistic language based on sampling functions
Sungwoo Park, Frank Pfenning, Sebastian Thrun
Article No.: 4
DOI: 10.1145/1452044.1452048

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...

Verified interoperable implementations of security protocols
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
Article No.: 5
DOI: 10.1145/1452044.1452049

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and...