Quantified Formulas in Interpolating SMT Solvers
Final Report Abstract
The goal of the research project was to develop interpolation algorithms for formulas in the combination of the Theory of Arrays with other theories. Interpolants are used in software model-checking to automatically generate correctness proofs of programs. When checking programs that use arrays or dynamic memory allocation, the resulting formulas usually require the Theory of Arrays to express the heap of a program. Thus our research directly contributed to software model-checking algorithms for real-world programs. In this project we developed an interpolation algorithm that takes a formula that corresponds to a trace of a program leading to an error, decides its feasibility, i. e., if there is a valuation for the program variables leading to the error. If the error trace is not feasible, the algorithm computes intermediate assertions (the so-called interpolants) that explain the absence of the error. These interpolants can then be used as candidates for program invariants to generalise from the proof of a single trace of the program to the whole program. In particular, we extended the existing algorithm for simple programs using finitely many variables, to array programs using dynamic memory allocations or large arrays. The first part of the project focused on quantifier-free formulas. Our algorithm improves on existing work that requires the solver to be modified for the interpolation problem. In particular, our solver is not aware of the interpolation problem and our interpolation engine produces several interpolants from the same proof (sequence and tree interpolants). As a surprise we found an error in previous literature that described an interpolation algorithm for quantifier-free array formulas. We showed that interpolants need exponentially many new terms in the worst case, which is in contradiction to Totla and Wies claiming that quadratically many new terms are enough. In the second part of the project we investigated solving and interpolation of quantified array formulas. Here we found that the array property fragment (that we originally planned to use) does not allow for interpolation: there are formulas in the array property fragment whose interpolant cannot be expressed in the array property fragment. We decided to extend the supported fragment to the full almost uninterpreted fragment, since this is expressive enough. The drawback is that this fragment is not decidable. Thus, the solving algorithm does not terminate for some input problems. We started a prototypical implementation for this fragment, which is still work in progress. In particular the proof generation is still not complete. Thus, our solver cannot produce interpolants.
Publications
- Efficient interpolation for the theory of arrays. CoRR, 2018
J. Hoenicke and T. Schindler
- Efficient interpolation for the theory of arrays. In IJCAR, volume 10900 of Lecture Notes in Computer Science, pages 549–565. Springer, 2018
J. Hoenicke and T. Schindler
(See online at https://doi.org/10.1007/978-3-319-94205-6_36) - Interpolation and the array property fragment. cs.LO, 2019
J. Hoenicke and T. Schindler
- Solving and interpolating constant arrays based on weak equivalences. In VMCAI, volume 11388 of Lecture Notes in Computer Science, pages 297–317. Springer, 2019
J. Hoenicke and T. Schindler
(See online at https://doi.org/10.1007/978-3-030-11245-5_14)
