**Date: **
17:30,
Tuesday, January 27, 2015

**Speaker: **
Helmut Seidl

**Venue: **TU Wien

**Notes: **

**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