<div class="csl-bib-body">
<div class="csl-entry">Zwirchmayr, J. (2013). <i>Symbolic methods for the timing analysis of programs</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22070</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2013.22070
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/8097
-
dc.description.abstract
In this thesis we present a method for proving WCET bounds precise. Our approach guarantees that the WCET bound is actually computed for a feasible trace in the system. Moreover, our method is able to improve the WCET analysis quality by reducing the required manual annotations and the imprecision of WCET estimates, automatically tightening the WCET bound until precise when necessary. For doing so, we apply and combine symbolic techniques from algorithmic combinatorics, computer algebra, automated theorem proving and for- mal methods. Such symbolic techniques usually yield good analysis information but are computationally expensive: symbolic execution, for example, requires path-wise execu- tion of the whole program. In order to overcome the computationally expensive costs of symbolic methods, our challenge is to identify and apply symbolic methods only on relevant program parts. This way, the precision of symbolic techniques is fully exploited while avoiding the computational costs of the underlying approaches.<br />
de
dc.description.abstract
In this thesis we present a method for proving WCET bounds precise. Our approach guarantees that the WCET bound is actually computed for a feasible trace in the system. Moreover, our method is able to improve the WCET analysis quality by reducing the required manual annotations and the imprecision of WCET estimates, automatically tightening the WCET bound until precise when necessary. For doing so, we apply and combine symbolic techniques from algorithmic combinatorics, computer algebra, automated theorem proving and for- mal methods. Such symbolic techniques usually yield good analysis information but are computationally expensive: symbolic execution, for example, requires path-wise execu- tion of the whole program. In order to overcome the computationally expensive costs of symbolic methods, our challenge is to identify and apply symbolic methods only on relevant program parts. This way, the precision of symbolic techniques is fully exploited while avoiding the computational costs of the underlying approaches.<br />
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
wcet analyse
de
dc.subject
programmanalyse
de
dc.subject
zeitanalyse
de
dc.subject
schleifenschranken
de
dc.subject
praezise wcet schranken
de
dc.subject
wcet analysis
en
dc.subject
program analysis
en
dc.subject
timing analysis
en
dc.subject
loop bounds
en
dc.subject
precise wcet bounds
en
dc.title
Symbolic methods for the timing analysis of programs