Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2011/12 / Oberseminar / Duma Rodriguez, Amortised Resource Analysis for Object-Oriented Programs


Duma Rodriguez, Amortised Resource Analysis for Object-Oriented Programs

TCS Oberseminar, 27.01.2012, 14:15 Uhr
Wann 14:10 15:15 27.01.2012
von bis
Wo L109
Termin übernehmen vCal

Dulma Rodriguez
Amortised Resource Analysis for Object-Oriented Programs

As software systems grow in size and complexity, the need for verifying some of their properties increases. One important property to be verified is the resource usage, where resources include execution time, memory, power, etc. Resource usage analysis is important in many areas, in particular embedded systems and cloud computing.

Resource Aware JAva (RAJA) is a type system for heap-space analysis of object-oriented programs, based on the amortised analysis technique. In this talk we present a type inference algorithm for the RAJA system. We were able to reduce the type inference problem to the novel problem of satisfiability of arithmetic constraints over infinite trees and we developed a heuristic algorithm for satisfiability of these constraints. We proved the soundness of the type inference algorithm and developed an Ocaml implementation and experimental evaluation that shows that we can compute linear upper-bounds to the heap-space requirements of many programs, including sorting algorithms for lists like insertion sort and merge sort and also programs that contain different interacting objects that describe real-life scenarios such as a bank account. Some of the programs consist of hundreds of lines of code and they could be analysed within a few seconds.

We also present a type checking algorithm for the RAJA system that is useful for verifying the types discovered by the type inference.


abgelegt unter: