Guiding Local Search using Approximations

Abstract: Proving that a program is correct can be done by translating it into a first-order formula and trying to prove that it is valid. Programs often contain data structures such as Floating-point numbers, for which current solvers struggle because of the computational complexity of these theories. By using approximations, the precision of the floating-point numbers can be reduced to lower the complexity making it easier for the solvers. If a solution to the approximate formula can be found, it is often close to a solution of the original formula. A reconstruction of this solution can be made by modifying it in different ways as an attempt to reconstruct it into a solution of the original formula. In this thesis a local-search algorithm is implemented as a reconstruction. By continuously keeping a candidate solution, starting with the approximate one it is possible to iteratively make small modifications to search for nearby candidates and eventually find a solution to the original formula. Three different configurations are implemented, evaluated against each other and also against existing reconstructions. Tests shows that a local-search reconstruction can be viable and opens up for further testing of different configurations.