Tuesday, January 27, 2015
Speaker: Helmut Seidl
Venue: TU Wien
Time: 17:30. Room: El 4. (Gußhausstrasse 25-29
2nd floor, room No. 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