In \Cref{ch:theory} the method of control-flow refinement via partial evaluation
was expanded to \acrfull{pip}. The method is proven to be sound for \gls{pip}s
and can be used to refine a \gls{pip} when classical analysis fails at finding
tight runtime bounds. In \Cref{ch:implementation} we have presented a new
implementation of partial evaluation on probabilistic programs and successfully
inferred tighter expected runtime complexity bounds for two probabilistic
examples.
\section{Future Work}\label{sec:future_work}
In \Cref{ch:preliminaries} and \Cref{ch:theory} we have skipped over the concept
of costs, which are closely related to runtime complexity. It is common to
assign costs to a transition which can vary depending on the value of program
variables. During a run of the program, those costs are added up for every
transition in the run. The runtime complexity of a program is a special
case of cost-analysis where every transition has costs equal to 1. Because the
costs would be equally copied from one transition to the unfolded transition, we
conjecture that the partial evaluation preserves worst-case expected costs
similarly to the worst-case expected runtime complexity. However, proving this
question needs additional research.
In \Sref{sec:performance}, we have seen that the new implementation is not as
good as iRankFinder on a small number of programs in the test sets. We tried to
mirror the behaviour of iRankFinder as closely as possible, but probably
deviated from it a significant way. For example, our implementation might
compute slightly different properties heuristically than iRankFinder's
implementation, or selecting the feedback set for locations had an unexpected
impact on the analysis. In any case, the worsened analysis results warrant
further investigation. Until then, \gls{koat} can keep using iRankFinder for
non-probabilistic integer programs.
During implementation, the constraints of versions are converted back and forth
to Aprons representation of polyhedra. There is room for improvement by
reducing the number of conversions to and from apron. Furthermore, the
satisfiability check for the constraint of a version is done twice. Once before
the unfolding and once after the unfolding during abstraction even though the
satisfiability after the unfolding is already implied. We can probably remove
one of the satisfiability checks and in turn reduce the number of calls to the
\gls{smt}-solver.
The heuristics used for property generation were taken over from
\citeauthor{Domenech19}, however in our implementation we found that the
heuristics resulted in a large number of properties and thus a larger than
probably necessary evaluation graph. With regard to sub-\gls{scc} level
evaluation, one could search for better heuristics which take the context of the
previous analysis into account in a more favourable way.
A last idea that came up during the writing of this thesis, is some sort of
online-abstraction. The localised property-based abstraction requires locations
to be selected for abstraction before the evaluation. Instead, one can imagine
an evaluation algorithm that abstracts only when traversing a loop on-the-fly,
even ignoring the first $k$ number of iterations and thus only abstracting when
really necessary. Such an online-abstraction could possibly increase the
precision of the partial evaluation even further. It is not immediately obvious
if this would improve the sub-\gls{scc} level analysis of \gls{koat} but this
might be interesting for some other class of program, we have not considered in
this thesis.
\section{Conclusion}\label{sec:conclusion}
Considering our goals, it was successfully proven in theory that partial
evaluation can be adapted to \glspl{pip}. The control-flow refinement technique
can be used when searching expected runtime complexity bounds of \glspl{pip}
since the expected runtime complexity bounds are preserved during partial
evaluation. With our new implementation, we successfully improved the runtime
performance of \gls{koat} during analysis of non-probabilistic integer programs.
In the future, our implementation can be used to replace iRankFinder, which is
used as a black-box at the moment. Furthermore, we have demonstrated that our
implementation for \glspl{pip} can be integrated into \gls{koat}'s analysis of
probabilistic integer programs and that tighter expected runtime complexity
bounds can be found on some programs. To the best of our knowledge, we applied
partial evaluation for the first time in a complexity analysis frame work for
probabilistic integer programs.