publication . Preprint . Part of book or chapter of book . 2018

Efficient Interpolation for the Theory of Arrays

Jochen Hoenicke; Tanja Schindler;
Open Access English
  • Published: 19 Apr 2018
Abstract
Existing techniques for Craig interpolation for the quantifier-free fragment of the theory of arrays are inefficient for computing sequence and tree interpolants: the solver needs to run for every partitioning $(A, B)$ of the interpolation problem to avoid creating $AB$-mixed terms. We present a new approach using Proof Tree Preserving Interpolation and an array solver based on Weak Equivalence on Arrays. We give an interpolation algorithm for the lemmas produced by the array solver. The computed interpolants have worst-case exponential size for extensionality lemmas and worst-case quadratic size otherwise. We show that these bounds are strict in the sense that ...
Subjects
ACM Computing Classification System: MathematicsofComputing_NUMERICALANALYSIS
free text keywords: Computer Science - Logic in Computer Science, Discrete mathematics, Craig interpolation, Weak equivalence, Extensionality, Exponential function, Solver, Interpolation, Memory safety, Computer science, Quadratic equation
Download fromView all 2 versions
http://arxiv.org/pdf/1804.0717...
Part of book or chapter of book
Provider: UnpayWall
http://link.springer.com/conte...
Part of book or chapter of book
Provider: Crossref
28 references, page 1 of 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.

28 references, page 1 of 2
Abstract
Existing techniques for Craig interpolation for the quantifier-free fragment of the theory of arrays are inefficient for computing sequence and tree interpolants: the solver needs to run for every partitioning $(A, B)$ of the interpolation problem to avoid creating $AB$-mixed terms. We present a new approach using Proof Tree Preserving Interpolation and an array solver based on Weak Equivalence on Arrays. We give an interpolation algorithm for the lemmas produced by the array solver. The computed interpolants have worst-case exponential size for extensionality lemmas and worst-case quadratic size otherwise. We show that these bounds are strict in the sense that ...
Subjects
ACM Computing Classification System: MathematicsofComputing_NUMERICALANALYSIS
free text keywords: Computer Science - Logic in Computer Science, Discrete mathematics, Craig interpolation, Weak equivalence, Extensionality, Exponential function, Solver, Interpolation, Memory safety, Computer science, Quadratic equation
Download fromView all 2 versions
http://arxiv.org/pdf/1804.0717...
Part of book or chapter of book
Provider: UnpayWall
http://link.springer.com/conte...
Part of book or chapter of book
Provider: Crossref
28 references, page 1 of 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.

28 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Preprint . Part of book or chapter of book . 2018

Efficient Interpolation for the Theory of Arrays

Jochen Hoenicke; Tanja Schindler;