
Research



Strategy Iteration

Strategy iteration is a method wellknown for finding optimal strategies for Markov decision processes.
It was observed by Gawlitza and Seidl that this method can be adapted and used for computing invariants in program analysis. The result was a maxstrategy improvement algorithm, which our work is based on. This algorithm performs a monotonic upward iteration over the lattice of template polyhedra, for example, by considering a series of wellchosen underapproximations of the original system (strategies). It is guaranteed to terminate and return the least fixed point w.r.t. the abstraction.
The following publications describe extensions of the original algorithm from purely numerical systems to logiconumerical systems (with Boolean and numerical variables):
 David Monniaux and Peter Schrammel. Speeding Up LogicoNumerical
Strategy Iteration. In Static Analysis, SAS'14, Vol. 8723 of LNCS, pp. 253267, Springer, 2014.
[bibtex]
[link]
[experiments]
 Peter Schrammel and Pavle Subotic. LogicoNumerical Strategy
Iteration. In Verification, Model Checking and Abstract
Interpretation, VMCAI'13, Vol. 7737 of LNCS, pp. 414433, Springer, 2013.
[bibtex]
[link]
[experiments]
A variant of the algorithm is used for inferring invariants in:
 Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel. Safety Verification and Refutation by kInvariants and kInduction. In Static Analysis, SAS'15, Vol. 9291 of LNCS, pp. 145161, Springer, 2015.
[bibtex]
[link]




Peter Schrammel







