# Efficient Interpolation for the Theory of Arrays

- Published: 19 Apr 2018

- 1
- 2

1. P. Andrianov, K. Friedberger, M. Mandrykin, V. Mutilin, and A. Volkov. CPABAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions. In TACAS (2), pages 355-359, 2017. [OpenAIRE]

2. D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. STTT, 9(5-6):505-525, 2007.

3. D. Beyer, S. L¨owe, and P. Wendler. Benchmarking and resource measurement. In SPIN, pages 160-178, 2015.

4. M. Bonacina and M. Johansson. On interpolation in automated theorem proving. J. Autom. Reasoning, 54(1):69-97, 2015.

5. A. Brillout, D. Kroening, P. Ru¨mmer, and T. Wahl. Program verification via Craig interpolation for Presburger arithmetic with arrays. In VERIFY@IJCAR, pages 31-46. EasyChair, 2010.

6. R. Bruttomesso, S. Ghilardi, and S. Ranise. Quantifier-free interpolation of a theory of arrays. Logical Methods in Computer Science, 8(2), 2012. [OpenAIRE]

7. R. Bruttomesso, S. Ghilardi, and S. Ranise. Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log., 15(1):5:1- 5:34, 2014. [OpenAIRE]

8. F. Cassez, A. Sloane, M. Roberts, M. Pigram, P. Suvanpong, and P. Gonz´alez de Aledo. Skink: Static analysis of programs in LLVM intermediate representation. In TACAS (2), pages 380-384, 2017.

9. J. Christ and J. Hoenicke. Instantiation-based interpolation for quantified formulae. In Decision Procedures in Software, Hardware and Bioware, volume 10161 of Dagstuhl Seminar Proceedings. Schloss Dagstuhl, Germany, 2010. [OpenAIRE]

10. J. Christ and J. Hoenicke. Weakly equivalent arrays. In FroCos, pages 119-134. Springer, 2015.

11. J. Christ and J. Hoenicke. Proof tree preserving tree interpolation. J. Autom. Reasoning, 57(1):67-95, 2016. [OpenAIRE]

12. J. Christ, J. Hoenicke, and A. Nutz. SMTInterpol: An interpolating SMT solver. In SPIN, pages 248-254. Springer, 2012. [OpenAIRE]

13. J. Christ, J. Hoenicke, and A. Nutz. Proof tree preserving interpolation. In TACAS, pages 124-138. Springer, 2013. [OpenAIRE]

14. M. Dangl, S. L¨owe, and P. Wendler. CPAchecker with support for recursive programs and floating-point arithmetic. In TACAS, pages 423-425. Springer, 2015.

15. A. Fuchs, A. Goel, J. Grundy, S. Krstic, and C. Tinelli. Ground interpolation for the theory of equality. Logical Methods in Computer Science, 8(1), 2012.

- 1
- 2

##### Related research

- 1
- 2

1. P. Andrianov, K. Friedberger, M. Mandrykin, V. Mutilin, and A. Volkov. CPABAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions. In TACAS (2), pages 355-359, 2017. [OpenAIRE]

2. D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. STTT, 9(5-6):505-525, 2007.

3. D. Beyer, S. L¨owe, and P. Wendler. Benchmarking and resource measurement. In SPIN, pages 160-178, 2015.

4. M. Bonacina and M. Johansson. On interpolation in automated theorem proving. J. Autom. Reasoning, 54(1):69-97, 2015.

5. A. Brillout, D. Kroening, P. Ru¨mmer, and T. Wahl. Program verification via Craig interpolation for Presburger arithmetic with arrays. In VERIFY@IJCAR, pages 31-46. EasyChair, 2010.

6. R. Bruttomesso, S. Ghilardi, and S. Ranise. Quantifier-free interpolation of a theory of arrays. Logical Methods in Computer Science, 8(2), 2012. [OpenAIRE]

7. R. Bruttomesso, S. Ghilardi, and S. Ranise. Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log., 15(1):5:1- 5:34, 2014. [OpenAIRE]

8. F. Cassez, A. Sloane, M. Roberts, M. Pigram, P. Suvanpong, and P. Gonz´alez de Aledo. Skink: Static analysis of programs in LLVM intermediate representation. In TACAS (2), pages 380-384, 2017.

9. J. Christ and J. Hoenicke. Instantiation-based interpolation for quantified formulae. In Decision Procedures in Software, Hardware and Bioware, volume 10161 of Dagstuhl Seminar Proceedings. Schloss Dagstuhl, Germany, 2010. [OpenAIRE]

10. J. Christ and J. Hoenicke. Weakly equivalent arrays. In FroCos, pages 119-134. Springer, 2015.

11. J. Christ and J. Hoenicke. Proof tree preserving tree interpolation. J. Autom. Reasoning, 57(1):67-95, 2016. [OpenAIRE]

12. J. Christ, J. Hoenicke, and A. Nutz. SMTInterpol: An interpolating SMT solver. In SPIN, pages 248-254. Springer, 2012. [OpenAIRE]

13. J. Christ, J. Hoenicke, and A. Nutz. Proof tree preserving interpolation. In TACAS, pages 124-138. Springer, 2013. [OpenAIRE]

14. M. Dangl, S. L¨owe, and P. Wendler. CPAchecker with support for recursive programs and floating-point arithmetic. In TACAS, pages 423-425. Springer, 2015.

15. A. Fuchs, A. Goel, J. Grundy, S. Krstic, and C. Tinelli. Ground interpolation for the theory of equality. Logical Methods in Computer Science, 8(1), 2012.

- 1
- 2