 |
Research
|
|
|
Strategy Iteration
|
Strategy iteration is a method well-known 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 max-strategy 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 well-chosen under-approximations 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 logico-numerical systems (with Boolean and numerical variables):
David Monniaux and Peter Schrammel. Speeding Up Logico-Numerical
Strategy Iteration. In Static Analysis, SAS'14, Vol. 8723 of LNCS, pp. 253-267, Springer, 2014.
[bibtex]
[link]
[experiments]
Peter Schrammel and Pavle Subotic. Logico-Numerical Strategy
Iteration. In Verification, Model Checking and Abstract
Interpretation, VMCAI'13, Vol. 7737 of LNCS, pp. 414-433, 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 k-Invariants and k-Induction. In Static Analysis, SAS'15, Vol. 9291 of LNCS, pp. 145-161, Springer, 2015.
[bibtex]
[link]
|
|
|
 |
Peter
Schrammel
|
|
|
|
|
|
|
|
|
|
|
|
