Search Results

Documents authored by Schordan, Markus

Document
DOI: 10.4230/OASIcs.WCET.2009.2282
From Trusted Annotations to Verified Knowledge

Authors: Adrian Prantl, Jens Knoop, Raimund Kirner, Albrecht Kadlec, and Markus Schordan

Published in: OASIcs, Volume 10, 9th International Workshop on Worst-Case Execution Time Analysis (WCET'09) (2009)

Abstract
WCET analyzers commonly rely on user-provided annotations such as loop bounds, recursion depths, region- and program constants. This reliance on user-provided annotations has an important drawback. It introduces a Trusted Annotation Basis into WCET analysis without any guarantee that the user-provided annotations are safe, let alone sharp. Hence, safety and accuracy of a WCET analysis cannot be formally established. In this paper we propose a uniform approach, which reduces the trusted annotation base to a minimum, while simultaneously yielding sharper (tighter) time bounds. Fundamental to our approach is to apply model checking in concert with other more inexpensive program analysis techniques, and the coordinated application of two algorithms for Binary Tightening and Binary Widening, which control the application of the model checker and hence the computational costs of the approach. Though in this paper we focus on the control of model checking by Binary Tightening and Widening, this is embedded into a more general approach in which we apply an array of analysis methods of increasing power and computational complexity for proving or disproving relevant time bounds of a program. First practical experiences using the sample programs of the Mälardalen benchmark suite demonstrate the usefulness of the overall approach. In fact, for most of these benchmarks we were able to empty the trusted annotation base completely, and to tighten the computed WCET considerably.
Cite as

Adrian Prantl, Jens Knoop, Raimund Kirner, Albrecht Kadlec, and Markus Schordan. From Trusted Annotations to Verified Knowledge. In 9th International Workshop on Worst-Case Execution Time Analysis (WCET'09). Open Access Series in Informatics (OASIcs), Volume 10, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{prantl_et_al:OASIcs.WCET.2009.2282,
  author =	{Prantl, Adrian and Knoop, Jens and Kirner, Raimund and Kadlec, Albrecht and Schordan, Markus},
  title =	{{From Trusted Annotations to Verified Knowledge}},
  booktitle =	{9th International Workshop on Worst-Case Execution Time Analysis (WCET'09)},
  pages =	{1--11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-14-9},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{10},
  editor =	{Holsti, Niklas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2009.2282},
  URN =		{urn:nbn:de:0030-drops-22828},
  doi =		{10.4230/OASIcs.WCET.2009.2282},
  annote =	{Keywords: WCET analysis, annotations, binary tightening, binary widening, model checking, CBMC}
}
Document
DOI: 10.4230/OASIcs.WCET.2008.1663
WCET 2008 -- Report from the Tool Challenge 2008 -- 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis

Authors: Niklas Holsti, Jan Gustafsson, Guillem Bernat, Clément Ballabriga, Armelle Bonenfant, Roman Bourgade, Hugues Cassé, Daniel Cordes, Albrecht Kadlec, Raimund Kirner, Jens Knoop, Paul Lokuciejewski, Nicholas Merriam, Marianne de Michiel, Adrian Prantl, Bernhard Rieder, Christine Rochange, Pascal Sainrat, and Markus Schordan

Published in: OASIcs, Volume 8, 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08) (2008)

Abstract
Following the successful WCET Tool Challenge in 2006, the second event in this series was organized in 2008, again with support from the ARTIST2 Network of Excellence. The WCET Tool Challenge 2008 (WCC'08) provides benchmark programs and poses a number of "analysis problems" about the dynamic, run-time properties of these programs. The participants are challenged to solve these problems with their program analysis tools. Two kinds of problems are defined: WCET problems, which ask for bounds on the execution time of chosen parts (subprograms) of the benchmarks, under given constraints on input data; and flow-analysis problems, which ask for bounds on the number of times certain parts of the benchmark can be executed, again under some constraints. We describe the organization of WCC'08, the benchmark programs, the participating tools, and the general results, successes, and failures. Most participants found WCC'08 to be a useful test of their tools. Unlike the 2006 Challenge, the WCC'08 participants include several tools for the same target (ARM7, LPC2138), and tools that combine measurements and static analysis, as well as pure static-analysis tools.
Cite as

Niklas Holsti, Jan Gustafsson, Guillem Bernat, Clément Ballabriga, Armelle Bonenfant, Roman Bourgade, Hugues Cassé, Daniel Cordes, Albrecht Kadlec, Raimund Kirner, Jens Knoop, Paul Lokuciejewski, Nicholas Merriam, Marianne de Michiel, Adrian Prantl, Bernhard Rieder, Christine Rochange, Pascal Sainrat, and Markus Schordan. WCET 2008 -- Report from the Tool Challenge 2008 -- 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. In 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08). Open Access Series in Informatics (OASIcs), Volume 8, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{holsti_et_al:OASIcs.WCET.2008.1663,
  author =	{Holsti, Niklas and Gustafsson, Jan and Bernat, Guillem and Ballabriga, Cl\'{e}ment and Bonenfant, Armelle and Bourgade, Roman and Cass\'{e}, Hugues and Cordes, Daniel and Kadlec, Albrecht and Kirner, Raimund and Knoop, Jens and Lokuciejewski, Paul and Merriam, Nicholas and de Michiel, Marianne and Prantl, Adrian and Rieder, Bernhard and Rochange, Christine and Sainrat, Pascal and Schordan, Markus},
  title =	{{WCET 2008 -- Report from the Tool Challenge 2008 -- 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis}},
  booktitle =	{8th International Workshop on Worst-Case Execution Time Analysis (WCET'08)},
  pages =	{1--23},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-10-1},
  ISSN =	{2190-6807},
  year =	{2008},
  volume =	{8},
  editor =	{Kirner, Raimund},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2008.1663},
  URN =		{urn:nbn:de:0030-drops-16637},
  doi =		{10.4230/OASIcs.WCET.2008.1663},
  annote =	{Keywords: WCET analysis, benchmark}
}
Document
DOI: 10.4230/OASIcs.WCET.2008.1657
Towards a Common WCET Annotation Language: Essential Ingredients

Authors: Raimund Kirner, Albrecht Kadlec, Adrian Prantl, Markus Schordan, and Jens Knoop

Published in: OASIcs, Volume 8, 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08) (2008)

Abstract
Within the last years, ambitions towards the definition of common interfaces and the development of open frameworks have increased the efficiency of research on WCET analysis. The Annotation Language Challenge for WCET analysis has been proposed in line with these ambitions in order to push the development of common interfaces also to the level of annotation languages, which are crucial for the power of WCET analysis tools. In this paper we present a list of essential ingredients for a common WCET annotation language. The selected ingredients comprise a number of features available in different WCET analysis tools and add several new concepts we consider important. The annotation concepts are described in an abstract format that can be instantiated at different representation levels.
Cite as

Raimund Kirner, Albrecht Kadlec, Adrian Prantl, Markus Schordan, and Jens Knoop. Towards a Common WCET Annotation Language: Essential Ingredients. In 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08). Open Access Series in Informatics (OASIcs), Volume 8, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{kirner_et_al:OASIcs.WCET.2008.1657,
  author =	{Kirner, Raimund and Kadlec, Albrecht and Prantl, Adrian and Schordan, Markus and Knoop, Jens},
  title =	{{Towards a Common WCET Annotation Language: Essential Ingredients}},
  booktitle =	{8th International Workshop on Worst-Case Execution Time Analysis (WCET'08)},
  pages =	{1--13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-10-1},
  ISSN =	{2190-6807},
  year =	{2008},
  volume =	{8},
  editor =	{Kirner, Raimund},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2008.1657},
  URN =		{urn:nbn:de:0030-drops-16575},
  doi =		{10.4230/OASIcs.WCET.2008.1657},
  annote =	{Keywords: Worst-case execution time (WCET) analysis, annotation languages, WCET annotation language challenge}
}
Document
DOI: 10.4230/OASIcs.WCET.2008.1661
TuBound - A Conceptually New Tool for Worst-Case Execution Time Analysis

Authors: Adrian Prantl, Markus Schordan, and Jens Knoop

Published in: OASIcs, Volume 8, 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08) (2008)

Abstract
TuBound is a conceptually new tool for the worst-case execution time (WCET) analysis of programs. A distinctive feature of TuBound is the seamless integration of a WCET analysis component and of a compiler in a uniform tool. TuBound enables the programmer to provide hints improving the precision of the WCET computation on the high-level program source code, while preserving the advantages of using an optimizing compiler and the accuracy of a WCET analysis performed on the low-level machine code. This way, TuBound ideally serves the needs of both the programmer and the WCET analysis by providing them the interface on the very abstraction level that is most appropriate and convenient to them. In this paper we present the system architecture of TuBound, discuss the internal work-flow of the tool, and report on first measurements using benchmarks from Maelardalen University. TuBound took also part in the WCET Tool Challenge 2008.
Cite as

Adrian Prantl, Markus Schordan, and Jens Knoop. TuBound - A Conceptually New Tool for Worst-Case Execution Time Analysis. In 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08). Open Access Series in Informatics (OASIcs), Volume 8, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{prantl_et_al:OASIcs.WCET.2008.1661,
  author =	{Prantl, Adrian and Schordan, Markus and Knoop, Jens},
  title =	{{TuBound - A Conceptually New Tool for Worst-Case Execution Time Analysis}},
  booktitle =	{8th International Workshop on Worst-Case Execution Time Analysis (WCET'08)},
  pages =	{1--8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-10-1},
  ISSN =	{2190-6807},
  year =	{2008},
  volume =	{8},
  editor =	{Kirner, Raimund},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2008.1661},
  URN =		{urn:nbn:de:0030-drops-16611},
  doi =		{10.4230/OASIcs.WCET.2008.1661},
  annote =	{Keywords: Worst-case execution time (WCET) analysis, Tool Chain, Flow Constraints, Source-To-Source}
}
Document
DOI: 10.4230/DagSemProc.08161.1
08161 Abstracts Collection – Scalable Program Analysis

Authors: Florian Martin, Hanne Riis Nielson, Claudio Riva, and Markus Schordan

Published in: Dagstuhl Seminar Proceedings, Volume 8161, Scalable Program Analysis (2008)

Abstract
From April 13 to April 18, 2008, the Dagstuhl Seminar 08161 ``Scalable Program Analysis'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Florian Martin, Hanne Riis Nielson, Claudio Riva, and Markus Schordan. 08161 Abstracts Collection – Scalable Program Analysis. In Scalable Program Analysis. Dagstuhl Seminar Proceedings, Volume 8161, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{martin_et_al:DagSemProc.08161.1,
  author =	{Martin, Florian and Riis Nielson, Hanne and Riva, Claudio and Schordan, Markus},
  title =	{{08161 Abstracts Collection – Scalable Program Analysis}},
  booktitle =	{Scalable Program Analysis},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8161},
  editor =	{Florian Martin and Hanne Riis Nielson and Claudio Riva and Markus Schordan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08161.1},
  URN =		{urn:nbn:de:0030-drops-15766},
  doi =		{10.4230/DagSemProc.08161.1},
  annote =	{Keywords: Static analysis, security, pointer analysis, data flow analysis, error detection, concurrency}
}
Document
DOI: 10.4230/DagSemProc.08161.7
Source-To-Source Analysis with SATIrE - an Example Revisited

Authors: Markus Schordan

Published in: Dagstuhl Seminar Proceedings, Volume 8161, Scalable Program Analysis (2008)

Abstract
Source-to-source analysis aims at supporting the reuse of analysis results similar to code reuse. The reuse of program code is a common technique which attempts to save time and costs by reducing redundant work. We want to avoid re-analyzing parts of a software system, such as library code. In the ideal case the analysis results are directly associated with the program itself. Source-to-source analysis supports this through program annotations. Further more, to get the best out of available software analysis tools, we aim at enabling the combination of the analysis results of different tools. In order to allow this, tools must be able to process another tool's analysis results. This enables numerous applications such as automatic annotation of interfaces, testing of analyses by checking the results of an analysis against provided annotations, domain aware analysis by utilizing domain-specific program annotations, and making analysis results persistent as annotations in source code. The design of the {em Static Analysis Tool Integration Engine} (SATIrE cite{satirewebsite}) allows to map source code annotations to its intermediate program representation as well as generating source code annotations from analysis results that are attached to the intermediate representation. The technical challenges are the design of the analysis information annotation language, the bidirectional propagation of the analysis information through different phases of the internal translation processes, and the combination of the different analyses through the plug-in mechanism. In its current version SATIrE targets C/C++ programs. In this paper we present the approach of source-to-source analysis and show in a detailed example analysis how we support this approach in SATIrE.
Cite as

Markus Schordan. Source-To-Source Analysis with SATIrE - an Example Revisited. In Scalable Program Analysis. Dagstuhl Seminar Proceedings, Volume 8161, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{schordan:DagSemProc.08161.7,
  author =	{Schordan, Markus},
  title =	{{Source-To-Source Analysis with SATIrE - an Example Revisited}},
  booktitle =	{Scalable Program Analysis},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8161},
  editor =	{Florian Martin and Hanne Riis Nielson and Claudio Riva and Markus Schordan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08161.7},
  URN =		{urn:nbn:de:0030-drops-15693},
  doi =		{10.4230/DagSemProc.08161.7},
  annote =	{Keywords: Source-to-source analysis, ARAL, Annotation Language}
}
Document
DOI: 10.4230/OASIcs.WCET.2007.1197
WCET Analysis: The Annotation Language Challenge

Authors: Raimund Kirner, Jens Knoop, Adrian Prantl, Markus Schordan, and Ingomar Wenzel

Published in: OASIcs, Volume 6, 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07) (2007)

Abstract
Worst-case execution time (WCET) analysis is indispensable for the successful design and development of systems, which, in addition to their functional constraints, have to satisfy hard real-time constraints. The expressiveness and usability of annotation languages, which are used by algorithms and tools for WCET analysis in order to separate feasible from infeasible program paths, have a crucial impact on the precision and performance of these algorithms and tools. In this paper, we thus propose to complement the WCET tool challenge, which has recently successfully been launched, by a second closely related challenge: the WCET annotation language challenge. We believe that contributions towards mastering this challenge will be essential for the next major step of advancing the field of WCET analysis.
Cite as

Raimund Kirner, Jens Knoop, Adrian Prantl, Markus Schordan, and Ingomar Wenzel. WCET Analysis: The Annotation Language Challenge. In 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07). Open Access Series in Informatics (OASIcs), Volume 6, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{kirner_et_al:OASIcs.WCET.2007.1197,
  author =	{Kirner, Raimund and Knoop, Jens and Prantl, Adrian and Schordan, Markus and Wenzel, Ingomar},
  title =	{{WCET Analysis: The Annotation Language Challenge}},
  booktitle =	{7th International Workshop on Worst-Case Execution Time Analysis (WCET'07)},
  pages =	{1--17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-05-7},
  ISSN =	{2190-6807},
  year =	{2007},
  volume =	{6},
  editor =	{Rochange, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2007.1197},
  URN =		{urn:nbn:de:0030-drops-11974},
  doi =		{10.4230/OASIcs.WCET.2007.1197},
  annote =	{Keywords: Worst-case execution time analysis, WCET, path description, annotation language challenge, expressiveness, convenience}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact