enter search term and/or author name
Symbolic bounds analysis of pointers, array indices, and accessed memory regions
Radu Rugina, Martin C. Rinard
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
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
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
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
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...