Resource Analysis

This page collects all the work done on the subject of resource analysis at Radboud University Nijmegen. This work is done within the context of the CHARTER and AHA projects, by researchers from the Digital Security group at the Institute for Computing and Information Sciences.

We have developed resource analysis methods based on polynomial interpolation and size-aware type-systems. First for a functional language, within the AHA project. Currently the focus is on Java programs, in the CHARTER project.

CHARTER

CHARTER - Critical and High Assurance Requirements Transformed through Engineering Rigour - is an ARTEMIS Embedded Computing Systems Initiative project.

CHARTER aims to develop concepts, methods, and tools for embedded system design and deployment that will enable developers to master the complexity and substantially improve the development, verification and certification of critical embedded systems.

Our goal within the CHARTER project is to develop polynomial loop-bounds analysis, size analysis and heap-space consumption analysis for Real-Time Java. So far, polynomial loop-bounds analysis has been established (see publications and prototypes below).

AHA

AHA (Amortised Heap Analysis) was a project that ran from 2006 to 2010. It was funded under grant nr. 612.063.511 by the Netherlands Organisation for Scientific Research (NWO).

The goal of AHA was to develop polynomial size analysis for a functional language.

Prototypes

ResAna Loop-Bounds Inference Prototype
Polynomial Size Analysis prototype

Publications

Interpolation-based Height Analysis for Improving a Recurrence Solver [pdf (The original publication is available at www.springerlink.com)] [presentation] [bibtex]
Manuel Montenegro, Olha Shkaravska, Marko van Eekelen, and Ricardo Peña
In Selected Revised Papers of the 2nd International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA 2011), Lecture Notes Computer Science 7177. Springer Verlag. To Appear.

Test-Based Inference of Polynomial Loop-Bound Functions [pdf] [presentation] [bibtex]
Olha Shkaravska, Rody Kersten and Marko van Eekelen
In PPPJ'10: Proceedings of the 8th International Conference on the Principles and Practice of Programming in Java, pages 99-108, 2010.

Collected Size Semantics for Functional Programs [pdf] [bibtex]
Olha Shkaravska, Marko van Eekelen and Alejandro Tamalet
In Proceedings of the 20th International Symposium on the Implementation and Application of Functional Languages, to appear.

Polynomial Size Analysis of First-Order Shapely Functions (revised) [pdf] [bibtex]
Olha Shkaravska, Marko van Eekelen and Ron van Kesteren
In Logical Methods in Computer Science, volume 5, issue 2, paper 10. Special Issue with Selected Papers from TLCA 2007. Pages 1-35, 2009

Size Analysis of Algebraic Data Types [pdf] [bibtex]
Alejandro Tamalet, Olha Shkaravska and Marko van Eekelen
In Trends in Functional Programming Volume 9, pages 33-48, Intellect Publishers, 2009.

Inferring Static Non-Monotonically Sized Types Through Testing (revised) [pdf] [bibtex]
Ron van Kesteren, Olha Shkaravska and Marko van Eekelen
In Revised Selected Papers of the 16th international Workshop on Functional and (Constraint) Logic Programming, Electronic Notes in Theoretical Computer Science, volume 216C, pages 45-63, Elsevier, 2008

AHA: Amortized Heap Space Usage Analysis [pdf] [bibtex]
Marko van Eekelen, Olha Shkaravska, Ron van Kesteren, Bart Jacobs, Erik Poll and Sjaak Smetsers
In Trends in Functional Programming volume 8, Selected Papers of the Eighth Symposium on Trends in Functional Programming, Intellect Publishers, pages 36-53, 2008.

Polynomial Size Analysis of First-Order Functions [pdf] [bibtex]
Olha Shkaravska, Ron van Kesteren and Marko van Eekelen
In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, LNCS 4583, Springer, pages 351-366 2007.

Inferring Static Non-Monotonically Sized Types Through Testing [pdf] [bibtex]
Ron van Kesteren, Olha Shkaravska and Marko van Eekelen
In Proceedings of the 16th international Workshop on Functional and (Constraint) Logic Programming, pages 123-139, 2007.

Technical reports

Univariate Polynomial Solutions of Nonlinear Polynomial Recurrence Relations. Techical Reports Radboud University Nijmegen, ICIS-R10003 [pdf, last update 12 March 2012]
Olha Shkaravska and Marko van Eekelen
Submitted to Journal of Symbolic Computations. Under Revision.
The accompanying this research Maple scripts are in [nonlindifeq.mw]

Ranking Functions for Loops with Disjunctive Exit-Conditions
[ pdf of the preproceedings]
Rody Kersten and Marko van Eekelen
In Ricardo Peña (ed.) Proceedings of the 2th International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA2011). Madrid, Spain.Tech. Rep. SIC-08/11. Dept. Computer Systems and Computing Universidad Complutense de Madrid. pp. 111-126. May 2011.