Description

Recently [1] we have shown that well known metrics and algorithms used in sparse matrix solvers can be applied in the context of software verification. An interesting continuation of this study is to find out if Multi-object optimization can be applied to reduce bandwidth, span and wavefront. A recent overview on bandwidth reduction [2] provides some pointers to meta heuristic algorithms. Furthermore a good starting point for an implementation is Mathlab: 

 - https://nl.mathworks.com/help/optim/ug/generate-and-plot-a-pareto-front.html.

 - https://www.mathworks.com/matlabcentral/fileexchange/47197-genetic-programming-matlab-toolbox

The goal of the research is to find out how wel Multi-objective optimization can be applied in the context of symbolic reachability analysis. Hopefully the algorithms produced in this research outperform currently implemented algorithms in LTSmin [3].

References

1. 1 (Digital version available here)
2. 2 (Digital version available here)
3. 3 (Digital version available here)