Interpolation results for arrays with length and maxdiff. (English) Zbl 07760989
References:
| [1] | 2021. AXDInterpolator. (2021). Retrieved December 10, 2021 from https://github.com/typesAreSpaces/AXDInterpolator. |
| [2] | Alberti, Francesco, Ghilardi, Silvio, and Pagani, Elena. 2017. Cardinality constraints for arrays (decidability results and applications). Formal Methods in System Design51, 3 (2017), 545-574. DOI: · Zbl 1377.68125 |
| [3] | Bacsich, Paul D.. 1975. Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis5 (1975), 45-55. · Zbl 0324.02036 |
| [4] | Beyer, Dirk. 2021. Software verification: 10th comparative evaluation (SV-COMP 2021). In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21), Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Vol. 12652. Springer, Berlin, 401-422. DOI: |
| [5] | Bradley, Aaron R., Manna, Zohar, and Sipma, Henny B.. 2006. What’s decidable about arrays?. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06), E. Allen Emerson and Kedar S. Namjoshi (Eds.). Vol. 3855. Springer, Berlin, 427-442. DOI: · Zbl 1176.68116 |
| [6] | Bruttomesso, Roberto, Cimatti, Alessandro, Franzén, Anders, Griggio, Alberto, and Sebastiani, Roberto. 2008. The MathSAT 4 SMT solver. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV’08), Aarti Gupta and Sharad Malik (Eds.). Vol. 5123. Springer, Berlin, 299-303. DOI: · Zbl 1165.68482 |
| [7] | Bruttomesso, Roberto, Ghilardi, Silvio, and Ranise, Silvio. 2012. Quantifier-free interpolation of a theory of arrays. Logical Methods in Computer Science8, 2 (2012), 1-39. DOI: · Zbl 1237.68123 |
| [8] | Bruttomesso, Roberto, Ghilardi, Silvio, and Ranise, Silvio. 2014. Quantifier-free interpolation in combinations of equality interpolating theories. ACM Transactions on Computational Logic15, 1 (2014), 5:1-5:34. DOI: · Zbl 1287.03068 |
| [9] | Castellanos Joo, José Abel, Ghilardi, Silvio, Gianola, Alessandro, and Kapur, Deepak. 2021. AXDInterpolator: A tool for computing interpolants for arrays with MaxDiff. In Proceedings of the 19th International Workshop on Satisfiability Modulo Theories (SMT’21), Vol. 2908. CEUR Workshop Proceedings, 40-52. http://ceur-ws.org/Vol-2908/paper15.pdf. |
| [10] | Chang, C. C. and Keisler, H. Jerome. 1990. Model Theory (3rd ed.). North-Holland, Amsterdam-London. · Zbl 0149.00402 |
| [11] | Christ, Jürgen, Hoenicke, Jochen, and Nutz, Alexander. 2012. SMTInterpol: An interpolating SMT solver. In Proceedings of the 19th International Workshop on Model Checking Software (SPIN’12), Alastair F. Donaldson and David Parker (Eds.). Vol. 7385. Springer, Berlin, 248-254. |
| [12] | Christ, Jürgen, Hoenicke, Jochen, and Nutz, Alexander. 2013. Proof tree preserving interpolation. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13), Nir Piterman and Scott A. Smolka (Eds.). Vol. 7795. Springer, Berlin, 124-138. DOI: · Zbl 1381.68152 |
| [13] | Craig, William. 1957. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic22 (1957), 269-285. · Zbl 0079.24502 |
| [14] | De Moura, Leonardo and Bjørner, Nikolaj. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), C. R. Ramakrishnan and Jakob Rehof (Eds.). Vol. 4963. Springer, 337-340. DOI: |
| [15] | Ghilardi, Silvio. 2004. Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning33, 3-4 (2004), 221-249. · Zbl 1069.03008 |
| [16] | Ghilardi, Silvio, Gianola, Alessandro, and Kapur, Deepak. 2021. Interpolation and amalgamation for arrays with MaxDiff. In Proceedings of the 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’21), Stefan Kiefer and Christine Tasson (Eds.). Vol. 12650. Springer, Berlin, 268-288. DOI: · Zbl 07410429 |
| [17] | Hoenicke, Jochen and Schindler, Tanja. 2018. Efficient interpolation for the theory of arrays. In Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR’18), Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.). Vol. 10900. Springer, Berlin, 549-565. DOI: · Zbl 1511.68314 |
| [18] | Hoenicke, Jochen and Schindler, Tanja. 2019. Interpolation and the array property fragment. CoRRabs/1904.11381 (2019). http://arxiv.org/abs/1904.11381. · Zbl 1522.68323 |
| [19] | Kapur, Deepak, Majumdar, Rupak, and Zarba, Calogero G.. 2006. Interpolation for data structures. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE’06). ACM, 105-116. |
| [20] | Kiss, Emil W., Márki, László, Pröhle, Péter, and Tholen, Walter. 1982. Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Studia Scientiarum Mathematicarum Hungarica18, 1 (1982), 79-140. SSMHAX · Zbl 0549.08001 |
| [21] | Krishnan, Hari Govind Vediramana, Vizel, Yakir, Ganesh, Vijay, and Gurfinkel, Arie. 2019. Interpolating strong induction. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV’19), Isil Dillig and Serdar Tasiran (Eds.). Vol. 11562. Springer, 367-385. DOI: · Zbl 1533.68166 |
| [22] | McCarthy, John. 1962. Towards a mathematical science of computation. In Proceedings of the 2nd Congress on Information Processing (IFIP’62). North-Holland, 21-28. |
| [23] | McMillan, Kenneth L.. 2003. Interpolation and SAT-based model checking. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03), Warren A. Hunt Jr. and Fabio Somenzi (Eds.). Vol. 2725. Springer, Berlin, 1-13. DOI: · Zbl 1278.68184 |
| [24] | McMillan, Kenneth L.. 2006. Lazy abstraction with interpolants. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06), Thomas Ball and Robert B. Jones (Eds.). Vol. 4144. Springer, Berlin, 123-136. · Zbl 1188.68196 |
| [25] | McMillan, Kenneth L.. 2011. Interpolants from Z3 proofs. In Proceedings of the 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD’11). FMCAD Inc., 19-27. |
| [26] | Nelson, Greg and Oppen, Derek C.. 1979. Simplification by cooperating decision procedures. ACM ACM Transactions on Programming Languages and Systems1, 2 (1979), 245-257. · Zbl 0452.68013 |
| [27] | Raya, Rodrigo and Kunkak, Viktor. 2022. NP satisfiability for arrays as powers. In Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’22), Bernd Finkbeiner and Thomas Wies (Eds.). Vol. 13182. Springer, Berlin, 301-318. DOI: · Zbl 1498.68127 |
| [28] | Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica. 2007. Constraint solving for interpolation. In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’07), Byron Cook and Andreas Podelski (Eds.). Vol. 4349. Springer, 346-362. DOI: · Zbl 1132.68480 |
| [29] | Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica. 2010. Constraint solving for interpolation. Journal of Symbolic Computation45, 11 (2010), 1212-1233. DOI: · Zbl 1213.68389 |
| [30] | Sofronie-Stokkermans, Viorica. 2006. Interpolation in local theory extensions. In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR’06), Ulrich Furbach and Natarajan Shankar (Eds.). Vol. 4130. Springer, Berlin, 235-250. DOI: · Zbl 1222.03018 |
| [31] | Sofronie-Stokkermans, Viorica. 2008. Interpolation in local theory extensions. Logical Methods in Computer Science4, 4 (2008), 1-31. DOI: · Zbl 1170.03018 |
| [32] | Sofronie-Stokkermans, Viorica. 2016. On interpolation and symbol elimination in theory extensions. In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR’16), Nicola Olivetti and Ashish Tiwari (Eds.). Vol. 9706. Springer, Berlin, 273-289. DOI: · Zbl 1476.03042 |
| [33] | Sofronie-Stokkermans, Viorica. 2018. On interpolation and symbol elimination in theory extensions. Logical Methods in Computer Science14, 3 (2018), 1-41. DOI: · Zbl 1476.03043 |
| [34] | Totla, Nishant and Wies, Thomas. 2013. Complete instantiation-based interpolation. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13). ACM, 537-548. DOI: · Zbl 1301.68106 |
| [35] | Totla, Nishant and Wies, Thomas. 2016. Complete instantiation-based interpolation. Journal of Automated Reasoning57, 1 (2016), 37-65. DOI: · Zbl 1356.68203 |
| [36] | Vizel, Yakir and Gurfinkel, Arie. 2014. Interpolating property directed reachability. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV’14), Armin Biere and Roderick Bloem (Eds.). 260-276. DOI: |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
