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 AHA, CHARTER and Go-Green 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.

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.

CHARTER

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

CHARTER aimed to develop concepts, methods, and tools for embedded system design and deployment that enable developers to master the complexity and substantially improve the development, verification and certification of critical embedded systems. In the context of the CHARTER project we have developed polynomial loop-bounds analysis and memory consumption analysis for (Real-Time) Java.

Go-Green

Go-Green is a dutch project, sponsored by Agentschap NL, which aims to develop an intelligent energy-aware system that learns people's behavior, understands their needs, provides reliable feedback in terms of best practices for energy use and distribution, intelligently harvests energy from various sources, and allows people to be in control. The system itself should be energy-neutral.

In the context of the Go-Green project we are developing an analysis for static estimation of energy-consumption of software, which is parametric with respect to hardware models as well as user-input.

Prototypes

ECAlogic
ResAna Loop-Bounds Inference Prototype
Polynomial Size Analysis prototype

Supporting material for topic Polynomial Solutions for Algebraic Difference Equations (ADE)

Symbolic calculations (Maxima script) related to ADE with CONSTANT coefficients
Symbolic calculations (Maxima script) related to ADE with VARIABLE coefficients
Running example (Maxima script)
Proof of the influence of G0(x)-term (Maxima Script)
Technical report Polynomial solutions of algebraic difference equations and homogeneous symmetric polynomials

Publications

ECAlogic: Hardware-Parametric Energy-Consumption Analysis of Algorithms [pdf][bibtex]
Marc Schoolderman, Jascha Neutelings, Rody Kersten and Marko van Eekelen
In Proceedings of the 13th Foundations of Aspect-Oriented Languages Workshop, pages 19-22, 2014.

A Hoare Logic for Energy Consumption Analysis [pdf][bibtex]
Rody Kersten, Paolo Parisen Toldin, Bernard van Gastel and Marko van Eekelen
In Proceedings of the Third International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'13), LNCS 8552, pages 93-109, 2014.

ResAna: A Resource Analysis Toolset for (Real-Time) Java [Early View Online]
Rody Kersten, Bernard van Gastel, Olha Shkaravska, Manuel Montenegro and Marko van Eekelen
Journal of Concurrency and Computation: Practice and Experience, Wiley. 24 pages. To appear.

Making Resource Analysis Practical for Real-Time Java [pdf][presentation][bibtex]
Rody Kersten, Olha Shkaravska, Bernard van Gastel, Manuel Montenegro and Marko van Eekelen
In JTRES'12: Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems, ACM Digital Proceedings Series, 2012.

Interpolation-based Height Analysis for Improving a Recurrence Solver [pdf] [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.

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 over Lists [pdf]
Olha Shkaravska, Marko van Eekelen and Alejandro Tamalet
In Selected Papers of the 20th Symposium on Implementation and Application of Functional Programming, IFL 2008, University of Hertfordshire, UK, 2008, LNCS, Volume 5836. Springer Verlag, pp. 118-137, 2011.

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]
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

Soundness Proof for a Hoare Logic for Energy Consumption Analysis [pdf][bibtex]
Paolo Parisen Toldin, Rody Kersten, Bernard van Gastel, and Marko van Eekelen
Technical report ICIS--R13009, Radboud University Nijmegen, October 2013.

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.

Univariate Polynomial Solutions of Nonlinear Polynomial Recurrence Relations [pdf, last update August 12, 2013]
Olha Shkaravska and Marko van Eekelen
Technical report ICIS--R10003, Radboud University Nijmegen, October 2010. Submitted to Journal of Symbolic Computations. Under Revision.
The Maple scripts accompanying this research are in [nonlindifeq.tar.gz]