July 16 – 21 , 2017, Dagstuhl Seminar 17291

Resource Bound Analysis


Marco Gaboardi (University at Buffalo, US)
Jan Hoffmann (Carnegie Mellon University – Pittsburgh, US)
Reinhard Wilhelm (Universität des Saarlandes, DE)
Florian Zuleger (TU Wien, AT)

For support, please contact

Dagstuhl Service Team


List of Participants
Shared Documents
Dagstuhl Seminar Wiki

(Use seminar number and access code to log in)


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.

  Creative Commons BY 3.0 DE
  Marco Gaboardi, Jan Hoffmann, Reinhard Wilhelm, and Florian Zuleger


  • Programming Languages / Compiler
  • Semantics / Formal Methods
  • Verification / Logic


  • Resource-Bound Analysis
  • WCET Analysis
  • Verification
  • Compilation
  • Quantitative Analysis
  • Static Analysis
  • Type Systems
  • Abstract Interpretation
  • Automata Theory
  • Control-Flow Analysis

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support