16. – 21. Juli 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)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 7, Issue 7 Dagstuhl Report
Gemeinsame Dokumente
Dagstuhl-Seminar Wiki

(Zum Einloggen bitte Seminarnummer und Zugangscode verwenden)


This seminar is dedicated to our friend and colleague Martin Hofmann (1965-2018). Martin's vision and ideas have shaped our community and the way resource analysis is performed and thought about. We are grateful for the time we spent with him and we will sorely miss his ingenuity, kindness, and enthusiasm.

There are great research opportunities in combining the three aforementioned approaches to resource bound analysis. The goal of the Dagstuhl seminar was to bring together leading researchers with different backgrounds in these three areas to address challenging open problems and to facilitate communication across research areas.

To this end, the program included seven tutorials on state-of-the-art techniques in the different communities, and short talks on concrete topics with potential for cross–fertilization. This included combining WCET analysis with higher-level bound analysis techniques, hardware-specific refinement of high-level cost models, and interaction of resource analysis with compilation. Additionally, the seminar included two tools sessions: the first was a presentation of the aiT tool of AbsInt by Simon Wegener; the second was a session with presentations of different tools from different participants. Finally, the seminar included a discussion on open problems in the different areas as well as open problems for cross-fertilization.

The tutorials, the talks solicited from the participants, and the tool and discussion sessions allowed us to identify topics which are of common interest to the three different communities. Some of these topics are

  • invariant and flow analysis,
  • constraint solving and
  • formalisms and logics for resource bounds.

Supporting information about program invariants and the possible control flow are often required by a resource analysis, e.g., the maximal value of a loop counter, or the infeasibility of a program path. The actual resource analysis is often reduced to solving a constraint system, e.g., using techniques from linear programming or recurrence equations. Verification logics for resource bounds as well as programming language formalisms are of common interest as they allow to specify or to guarantee that a program satisfies a required worst case resource bound.

We believe that the further study of these topics promises to increase the connections and to leverage the synergies between the different communities.

Summary text license
  Creative Commons BY 3.0 Unported license
  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


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.