We present a new solver and interpolation algorithm for the theory of arrays with constant arrays. It is based on our previous work on weakly equivalent arrays. Constant arrays store the same value at every index, which is useful for model checking of programs with initialised memory. Instead of using a store chain to explicitly initialise the memory, using a constant array can considerably simplify the queries and thus reduce the solving and interpolation time. We show that only a few new rules are required for constant arrays and prove the correctness of the decision procedure and the interpolation procedure. We implemented the algorithm in our interpolating solver SMTInterpol.
CITATION STYLE
Hoenicke, J., & Schindler, T. (2019). Solving and interpolating constant arrays based on weak equivalences. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11388 LNCS, pp. 297–317). Springer Verlag. https://doi.org/10.1007/978-3-030-11245-5_14
Mendeley helps you to discover research relevant for your work.