×

Solving and interpolating constant arrays based on weak equivalences. (English) Zbl 1522.68323

Enea, Constantin (ed.) et al., Verification, model checking, and abstract interpretation. 20th international conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11388, 297-317 (2019).
Summary: 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 [Lect. Notes Comput. Sci. 10900, 549–565 (2018; Zbl 1511.68314)]. 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.
For the entire collection see [Zbl 1409.68014].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03C40 Interpolation, preservation, definability
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Citations:

Zbl 1511.68314
PDFBibTeX XMLCite
Full Text: DOI