|
Descripción
|
|
|---|---|
| Static analysis is a powerful technique used traditionally for optimizing programs, and, more recently, in tools to aid the software development process, and in partic- ular, in finding bugs and security vulnerabilities. More concretely, the importance of static analyses that can infer information about the costs of computations is well recognized since such information is very useful in a large number of applications. Furthermore, the increasing relevance of analysis applications such as static debug- ging, resource bounds certification of mobile code, and granularity control in parallelcomputing makes it interesting to develop analyses for resource notions that are ac- tually application-dependent. This may include, for example, bytes sent or received by an application, number of files left open, number of SMSs sent or received, energy consumption, number of accesses to a database, etc. In this thesis, we present a resource usage analysis that aims at inferring upper and lower bounds on the cost of programs as a function of its data size for a given set of user-definable resources of interest. We use logic programming as our basic paradigm since it subsumes many others and this allows us treating the problem at a considerable level of generality. Resource usage analysis requires various pre-analysis steps. An important one is Set-Sharing analysis which attempts to detect mode information and which vari- ables do not point to the same memory location, providing essential information to the resource usage analysis. Hence, this thesis also investigates the problem of ef- ficient Set-Sharing analyses presenting two different alternatives: (1) via widening operators, and (2) defining compact and effective encodings. Moving to the area of applications, a very interesting class involves certification of the resources used by mobile code. In this context, Java bytecode is widely used, mainly due to its security features and the fact that it is platform independent. Therefore, this thesis finally presents a resource usage analysis tool for Java bytecode that includes also a transformation which provides a block-level view of the bytecode, and can be used as a basis for developing analyses. We have also developed for this purpose, a generic, abstract interpretation-based fixpoint algorithm which is parametric in the abstract domain. By plugging appropriate abstract domains into it, the framework provides useful information that can improve the accuracy of the resource usage information. | |
|
Internacional
|
Si |
|
ISBN
|
|
|
Tipo de Tesis
|
Doctoral |
|
Calificación
|
Sobresaliente cum laude |
|
Fecha
|
|