Parametric Strategy Iteration
Program behavior may depend on parameters, which are either configured before compilation time, or provided at runtime, e.g., by sensors or other input devices.
- Starts at
TU Wien, Campus Gußhaus
EI 4 Reithoffer-Hörsaal
1040 Vienna, Gußhausstraße 25
Stiege 8, 2. Stock, CF0245
Program behavior may depend on parameters, which are either configured before compilation time, or provided at runtime, e.g., by sensors or other input devices. Parametric program analysis explores how different parameter settings may affect the program behavior.
In order to infer invariants depending on parameters, we introduce parametric strategy iteration. This algorithm determines the precise least solution of systems of integer equations depending on surplus parameters. Conceptually, our algorithm performs ordinary strategy iteration on the given integer system for all possible parameter settings in parallel. This is made possible by means of region trees to represent the occurring piecewise affine functions. We indicate that each required operation on these trees is polynomial-time if only constantly many parameters are involved.
Parametric strategy iteration for systems of integer equations allows to construct parametric integer interval analysis as well as parametric analysis of differences of integer variables. It thus provides a general technique to realize precise parametric program analysis if numerical properties of integer variables are of concern.
Joint work with: Thomas Gawlitza and Martin Schwarz
- Helmut Seidl, TU Munich
Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!