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


Dagstuhl Report, Volume 7, Issue 7 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Wiki

(Use seminar number and access code to log in)


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 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).

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.


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