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 27 Issue 2, March 2005

Symbolic bounds analysis of pointers, array indices, and accessed memory regions
Radu Rugina, Martin C. Rinard
Pages: 185-235
DOI: 10.1145/1057387.1057388
This article presents a novel framework for the symbolic bounds analysis of pointers, array indices, and accessed memory regions. Our framework formulates each analysis problem as a system of inequality constraints between symbolic bound polynomials....

Dealing with incomplete knowledge on CLP(FD) variable domains
Marco Gavanelli, Evelina Lamma, Paola Mello, Michela Milano
Pages: 236-263
DOI: 10.1145/1057387.1057389
Constraint Logic Programming languages on Finite Domains, CLP(FD), provide a declarative framework for Artificial Intelligence problems. However, in many real life cases, domains are not known and must be acquired or computed. In systems that...

Resource usage analysis
Atsushi Igarashi, Naoki Kobayashi
Pages: 264-313
DOI: 10.1145/1057387.1057390
It is an important criterion of program correctness that a program accesses resources in a valid manner. For example, a memory region that has been allocated should eventually be deallocated, and after the deallocation, the region should no longer be...

Polymorphic predicate abstraction
Thomas Ball, Todd Millstein, Sriram K. Rajamani
Pages: 314-343
DOI: 10.1145/1057387.1057391
Predicate abstraction is a technique for creating abstract models of software that are amenable to model checking algorithms. We show how polymorphism, a well-known concept in programming languages and program analysis, can be incorporated in a...

A systematic approach to static access control
François Pottier, Christian Skalka, Scott Smith
Pages: 344-382
DOI: 10.1145/1057387.1057392
The Java Security Architecture includes a dynamic mechanism for enforcing access control checks, the so-called stack inspection process. While the architecture has several appealing features, access control checks are all implemented via...