Abstract
In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.
The third author has been partially supported by the National Science Foundation CCF award 1908804.
Chapter PDF
Similar content being viewed by others
References
AXDInterpolator, https://github.com/typesAreSpaces/AXDInterpolator, accessed: 2020-10-12
Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Proc. of LPAR-18. LNCS, vol. 7180, pp. 46–61. Springer (2012). https://doi.org/10.1007/978-3-642-28717-6_7
Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Proc. of CAV. LNCS, vol. 7358, pp. 679–685. Springer (2012). https://doi.org/10.1007/978-3-642-31424-7_49
Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014)
Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification framework for array programs. In: Proc. of ATVA. LNCS, vol. 8837, pp. 18–23. Springer (2014). https://doi.org/10.1007/978-3-319-11936-6_2
Bacsich, P.D.: Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis 5, 45–55 (1975)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Proc. of VMCAI. LNCS, vol. 3855, pp. 427–442. Springer (2006). https://doi.org/10.1007/11609773_28
Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation of a theory of arrays. Log. Methods Comput. Sci. 8(2) (2012)
Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1), 5:1–5:34 (2014)
Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Proc. of CADE. LNCS (LNAI), vol. 11716, pp. 142–160. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_9
Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Combined covers and Beth definability. In: Proc. of IJCAR. LNCS (LNAI), vol. 12166, pp. 181–200. Springer (2020). https://doi.org/10.1007/978-3-030-51074-9_11
Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, uniform interpolants and superposition calculus (with applications to verificaton of data-aware processes). J. Autom. Reasoning (To appear)
Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: Proc. of TACAS. LNCS, vol. 12078, pp. 22–39. Springer (2020). https://doi.org/10.1007/978-3-030-45190-5_2
Chang, C.C., Keisler, H.J.: Model Theory. North-Holland Publishing Co., Amsterdam-London, third edn. (1990)
Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22, 269–285 (1957)
Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Proc. of CAV. LNCS, vol. 11561, pp. 259–277. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_14
Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reasoning 33(3-4), 221–249 (2004)
Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (the non-disjoint signatures case). In: Proc. of FroCoS. LNCS (LNAI), vol. 10483, pp. 316–332. Springer (2017). https://doi.org/10.1007/978-3-319-66167-4_18
Ghilardi, S., Gianola, A.: Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Logic 169(8), 731–754 (2018)
Ghilardi, S., Gianola, A., Kapur, D.: Computing uniform interpolants for EUF via (conditional) DAG-based compact representations. In: Proc. of CILC. CEUR Workshop Proceedings, vol. 2710, pp. 67–81. CEUR-WS.org (2020)
Ghilardi, S., Gianola, A., Kapur, D.: Interpolation and amalgamation for Arrays with MaxDiff (extended version). Technical Report \({\rm arXiv{:}2010.07082}\), \({\rm arXiv{.}org}\) (2020), https://arxiv.org/abs/2010.07082
Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Proc. of ATVA. LNCS, vol. 11138, pp. 248–266. Springer (2018). https://doi.org/10.1007/978-3-030-01090-4_15
Hoenicke, J., Schindler, T.: Efficient interpolation for the theory of arrays. In: Proc. of IJCAR. LNCS (LNAI), vol. 10900, pp. 549–565. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_36
Huang, G.: Constructing Craig interpolation formulas. In: Computing and Combinatorics COCOON. LNCS, vol. 959, pp. 181–190. Springer (1995). https://doi.org/10.1007/BFb0030832
Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Shoham, S.: Putting the squeeze on array programs: Loop verification via inductive rank reduction. In: Proc. of VMCAI. LNCS, vol. 11990, pp. 112–135. Springer (2020). https://doi.org/10.1007/978-3-030-39322-9_6
Kapur, D.: Nonlinear polynomials, interpolants and invariant generation for system analysis. In: Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with ISSAC (2017)
Kapur, D.: Conditional congruence closure over uninterpreted and interpreted symbols. J. Systems Science & Complexity 32(1), 317–355 (2019)
Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for Data Structures. In: Proc. of SIGSOFT-FSE. pp. 105–116. ACM (2006)
Krishnan, H.G.V., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: Proc. of CAV. LNCS, vol. 11562, pp. 367–385. Springer (2019). https://doi.org/10.1007/978-3-030-25543-5_21
McCarthy, J.: Towards a Mathematical Science of Computation. In: IFIP Congress. pp. 21–28 (1962)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. of CAV. LNCS, vol. 2725, pp. 1–13. Springer (2003). https://doi.org/10.1007/978-3-540-45069-6_1
McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. of CAV. LNCS, vol. 4144, pp. 123–136. Springer (2006). https://doi.org/10.1007/11817963_14
Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–57 (1979)
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997)
Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Log. Methods Comput. Sci. 4(4) (2008)
Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3) (2018)
Totla, N., Wies, T.: Complete instantiation-based interpolation. J. Autom. Reasoning 57(1), 37–65 (2016)
Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: Proc. of CAV. LNCS, vol. 8559, pp. 260–276. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_17
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Ghilardi, S., Gianola, A., Kapur, D. (2021). Interpolation and Amalgamation for Arrays with MaxDiff. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)