Programming Languages and Systems (TOPLAS)


Search Issue
enter search term and/or author name


ACM Transactions on Programming Languages and Systems (TOPLAS) - Special Issue ESOP'05, Volume 29 Issue 5, August 2007

Introduction to special ESOP'05 issue
Mooly Sagiv
Article No.: 23
DOI: 10.1145/1275497.1275498

BI-hyperdoctrines, higher-order separation logic, and abstraction
Bodil Biering, Lars Birkedal, Noah Torp-Smith
Article No.: 24
DOI: 10.1145/1275497.1275499

We present a precise correspondence between separation logic and a simple notion of predicate BI, extending the earlier correspondence given between part of separation logic and propositional BI. Moreover, we introduce the notion of...

A type discipline for authorization policies
Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
Article No.: 25
DOI: 10.1145/1275497.1275500

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as digital signatures, local ACLs, and encrypted...

The trace partitioning abstract domain
Xavier Rival, Laurent Mauborgne
Article No.: 26
DOI: 10.1145/1275497.1275501

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

A new foundation for control dependence and slicing for modern program structures
Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, John Hatcliff, Matthew B. Dwyer
Article No.: 27
DOI: 10.1145/1275497.1275502

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

Enforcing resource bounds via static verification of dynamic checks
Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula
Article No.: 28
DOI: 10.1145/1275497.1275503

We show how to limit a program's resource usage in an efficient way, using a novel combination of dynamic checks and static analysis. Usually, dynamic checking is inefficient due to the overhead of checks, while static analysis is difficult and...

Analysis of modular arithmetic
Markus Müller-Olm, Helmut Seidl
Article No.: 29
DOI: 10.1145/1275497.1275504

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 Zm of integers...