16.07.17 - 21.07.17, Seminar 17291

Resource Bound Analysis

The following text appeared on our web pages prior to the seminar, and was included as part of the invitation.

Motivation

The quality of software crucially depends on the amount of resources – such as time, memory, and energy – that are required for its execution. Understanding and bounding resource usage is not only crucial for writing efficient software but also to ensure correctness, safety, and security of software systems. Since derivation of precise bounds appears to be unfeasible in practice in all but the simplest cases, computer support for deriving resource bounds is highly desirable. However, despite major successes, it remains a great challenge to develop sound tools and techniques that aid developers in resource bound analysis.

One reason for the complexity of resource analysis is the need to take into account the complete software stack from the hardware, to the operating system, to high-level programming languages. As a result, resource bound analysis is studied in formal methods and programming languages at different levels of abstraction. This ranges from concrete clock-cycle bounds on specific hardware (WCET analysis), to high-level symbolic bound analysis (recurrence relations, type systems, abstract interpretation, term rewriting), to logical characterizations of asymptotic complexity (linear logic, type systems, semantics). These are active areas of research and there has been significant progress in all of them over the past decade. However, the research is mainly driven by separate communities with few interaction and collaboration between the different research areas.

The goal of this seminar is to bring together leading researchers with different backgrounds in resource bound analysis to address challenging open problems and to facilitate communication across research areas. To this end, the seminar will educate the participants about state-of-the-art techniques in the different communities. Moreover we plan to focus on several concrete topics including:

  • combining WCET analysis and symbolic bound analysis,
  • hardware-specific refinement of high-level cost models,
  • interaction of resource bound analysis and compilation,
  • high-level programming language support for resource analysis,
  • new applications for resource analysis, and
  • interaction of resource bound analysis and runtime systems.

The seminar will foster the discussion around these great research opportunities.

We hope that this seminar will start a continuous exchange of ideas across areas that will lead to solutions of problems in resource bound analysis that are currently out of reach.

License
Creative Commons BY 3.0 Unported license
Marco Gaboardi, Jan Hoffmann, Reinhard Wilhelm, and Florian Zuleger