Dagstuhl Seminar 17291
Resource Bound Analysis
( Jul 16 – Jul 21, 2017 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/17291
Organizers
- 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)
Contact
- Michael Gerke (for scientific matters)
- Annette Beyer (for administrative matters)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR 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
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.
Marco Gaboardi, Jan Hoffmann, Reinhard Wilhelm, and Florian Zuleger
- Sebastian Altmeyer (University of Amsterdam, NL) [dblp]
- Robert Atkey (University of Strathclyde - Glasgow, GB) [dblp]
- Martin Avanzini (Universität Innsbruck, AT) [dblp]
- Gilles Barthe (IMDEA Software - Madrid, ES) [dblp]
- Marc Brockschmidt (Microsoft Research UK - Cambridge, GB) [dblp]
- Hugues Cassé (University of Toulouse, FR) [dblp]
- Stephen Chong (Harvard University - Cambridge, US) [dblp]
- Ezgi Cicek (MPI-SWS - Saarbrücken, DE) [dblp]
- Ugo Dal Lago (University of Bologna, IT) [dblp]
- Norman Danner (Wesleyan Univ. - Middletown, US) [dblp]
- Ankush Das (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Marco Gaboardi (University at Buffalo, US) [dblp]
- Deepak Garg (MPI-SWS - Saarbrücken, DE) [dblp]
- Samir Genaim (Complutense University of Madrid, ES) [dblp]
- Dan R. Ghica (University of Birmingham, GB) [dblp]
- Jürgen Giesl (RWTH Aachen, DE) [dblp]
- Sebastian Hahn (Universität des Saarlandes, DE) [dblp]
- Reiner Hähnle (TU Darmstadt, DE) [dblp]
- Kevin Hammond (University of St. Andrews, GB) [dblp]
- Manuel Hermenegildo (IMDEA Software - Madrid, ES) [dblp]
- Jan Hoffmann (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Martin Hofmann (LMU München, DE) [dblp]
- Steffen Jost (LMU München, DE) [dblp]
- Zachary Kincaid (Princeton University, US) [dblp]
- Jens Knoop (TU Wien, AT) [dblp]
- Björn Lisper (Mälardalen University - Västerås, SE) [dblp]
- Yu David Liu (Binghamton University, US) [dblp]
- Alexey Loginov (GrammaTech Inc. - Ithaca, US) [dblp]
- Hans-Wolfgang Loidl (Heriot-Watt University - Edinburgh, GB) [dblp]
- Antonio Flores Montoya (TU Darmstadt, DE) [dblp]
- Georg Moser (Universität Innsbruck, AT) [dblp]
- Van Chan Ngo (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Jan Reineke (Universität des Saarlandes, DE) [dblp]
- Thomas W. Reps (University of Wisconsin - Madison, US) [dblp]
- Christine Rochange (University of Toulouse, FR) [dblp]
- Claudio Sacerdoti Coen (University of Bologna, IT) [dblp]
- Marko van Eekelen (University of Nijmegen, NL) [dblp]
- Pedro B. Vasconcelos (University of Porto, PT) [dblp]
- Marcus Völp (University of Luxembourg, LU) [dblp]
- Peter Wägemann (Universität Erlangen-Nürnberg, DE) [dblp]
- Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
- Lukasz Ziarek (University at Buffalo, US) [dblp]
- Florian Zuleger (TU Wien, AT) [dblp]
Classification
- programming languages / compiler
- semantics / formal methods
- verification / logic
Keywords
- Resource-Bound Analysis
- WCET Analysis
- Verification
- Compilation
- Quantitative Analysis
- Static Analysis
- Type Systems
- Abstract Interpretation
- Automata Theory
- Control-Flow Analysis
