{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:53Z","timestamp":1762459313750,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,11,17]],"date-time":"2015-11-17T00:00:00Z","timestamp":1447718400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-14-LAB3-0007"],"award-info":[{"award-number":["ANR-14-LAB3-0007"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-12-INSE-0010"],"award-info":[{"award-number":["ANR-12-INSE-0010"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10817-015-9352-2","type":"journal-article","created":{"date-parts":[[2015,11,17]],"date-time":"2015-11-17T01:39:27Z","timestamp":1447724367000},"page":"387-457","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Adding Decision Procedures to SMT Solvers Using Axioms with Triggers"],"prefix":"10.1007","volume":"56","author":[{"given":"Claire","family":"Dross","sequence":"first","affiliation":[]},{"given":"Sylvain","family":"Conchon","sequence":"additional","affiliation":[]},{"given":"Johannes","family":"Kanig","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,17]]},"reference":[{"key":"9352_CR1","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 8413, pp. 15\u201330. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54862-8_2"},{"key":"9352_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140\u2013164 (2003). In: 12th International Conference on Rewriting Techniques and Applications (RTA 2001)","DOI":"10.1016\/S0890-5401(03)00020-8"},{"key":"9352_CR3","doi-asserted-by":"crossref","unstructured":"Bansal, K., Reynolds, A., King, T., Barrett, C., Wies, T.: Deciding local theory extensions via E-matching. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, CAV 2015, Lecture Notes in Computer Science. Vol. 9207, pp.87\u2013105 Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_6"},{"key":"9352_CR4","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification. Lecture Notes in Computer Science","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer, Berlin (2011)"},{"key":"9352_CR5","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard version 2.0. Technical report, University of Iowa (2010)"},{"key":"9352_CR6","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"9352_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.: Engineering theories with Z3. In: Yang, H. (ed.) Proceedings of the 9th Asian Symposium on Programming Languages and Systems, APLAS 2011, Lecture Notes in Computer Science, vol. 7078, pp. 4\u201316. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-25318-8_3"},{"key":"9352_CR8","doi-asserted-by":"crossref","unstructured":"Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: SMT\u201908, ACM ICPS, vol. 367, pp. 1\u20135. ACM, New York (2008)","DOI":"10.1145\/1512464.1512466"},{"key":"9352_CR9","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006). Lecture Notes in Computer Science, vol. 3855, pp. 427\u2013442. Springer, Berlin (2006)","DOI":"10.1007\/11609773_28"},{"issue":"2","key":"9352_CR10","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s10009-009-0098-1","volume":"11","author":"S Chatterjee","year":"2009","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: A low-level memory model and an accompanying reachability predicate. Int. J. Softw. Tools Technol. Transf. 11(2), 105\u2013116 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9352_CR11","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE-21, LNCS, vol. 4603, pp. 183\u2013198. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"9352_CR12","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Engineering DPLL(T) $$+$$ + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008, LNCS, vol. 5195, pp. 475\u2013490. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71070-7_40"},{"key":"9352_CR13","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C. R., Rehof, J. (eds.) TACAS 2008, LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9352_CR14","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer-Aided Design, 2009. FMCAD 2009, pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"3","key":"9352_CR15","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"9352_CR16","unstructured":"Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Reasoning with triggers. In: 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, pp. 22\u201331 (2012)"},{"key":"9352_CR17","doi-asserted-by":"crossref","unstructured":"Dross, C., Filli\u00e2tre, J.C., Moy, Y.: Correct code containing containers. In: Gogolla, M., Wolff, B. (eds.) Proceedings of the 5th International Conference on Tests and Proofs, TAP\u201911, Lecture Notes in Computer Science, vol. 6706, pp. 102\u2013118. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-21768-5_9"},{"key":"9352_CR18","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, Lecture Notes in Computer Science, vol. 4246, pp. 497\u2013511. Springer, Berlin (2006)","DOI":"10.1007\/11916277_34"},{"key":"9352_CR19","doi-asserted-by":"crossref","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE-21, LNCS, vol. 4603, pp. 167\u2013182. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"9352_CR20","doi-asserted-by":"crossref","unstructured":"Ge, Y., de\u00a0Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, LNCS, vol. 5643, pp. 306\u2013320. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"9352_CR21","doi-asserted-by":"crossref","unstructured":"Goel, A., Krsti\u0107, S., Fuchs, A.: Deciding array formulas with frugal axiom instantiation. In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, ACM ICPS, pp. 12\u201317. ACM, New York (2008)","DOI":"10.1145\/1512464.1512468"},{"key":"9352_CR22","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Kuncak, V.: Towards complete reasoning about axiomatic specifications. In: Jhala, R., Schmidt, D. (eds.) Proceedings of VMCAI-12, LNCS, vol. 6538, pp. 278\u2013293. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-18275-4_20"},{"key":"9352_CR23","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Automation of Reasoning, Symbolic Computation, pp. 342\u2013376. Springer, Berlin (1983)","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"9352_CR24","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver\u2014an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, (IJCAR 2008), Lecture Notes in Computer Science, vol. 5195, pp. 292\u2013298. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"9352_CR25","doi-asserted-by":"crossref","unstructured":"Korovin, K.: Instantiation-based reasoning: from theory to practice. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction, CADE\u201922, Lecture Notes in Computer Science, vol. 5663, pp. 163\u2013166. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02959-2_14"},{"key":"9352_CR26","doi-asserted-by":"crossref","unstructured":"Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 7\u201316. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029813"},{"issue":"7","key":"9352_CR27","doi-asserted-by":"crossref","first-page":"1026","DOI":"10.1016\/j.ic.2011.03.005","volume":"209","author":"C Lynch","year":"2011","unstructured":"Lynch, C., Ranise, S., Ringeissen, C., Tran, D.K.: Automatic decidability and combinability. Inf. Comput. 209(7), 1026\u20131047 (2011)","journal-title":"Inf. Comput."},{"key":"9352_CR28","doi-asserted-by":"crossref","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani,S.K. (eds.) Computer Aided Verification, CAV 2005, Lecture Notes in Computer Science, vol. 3576, pp. 476\u2013490. Springer, Berlin (2005)","DOI":"10.1007\/11513988_47"},{"key":"9352_CR29","doi-asserted-by":"crossref","unstructured":"Moskal, M.: Programming with triggers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, ACM ICPS, pp. 20\u201329. ACM, New York (2009)","DOI":"10.1145\/1670412.1670416"},{"key":"9352_CR30","unstructured":"Nelson, G.: Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center (1981)"},{"issue":"6","key":"9352_CR31","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9352_CR32","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, CAV 2013, Lecture Notes in Computer Science, Vol. 8044, pp. 773\u2013789. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"9352_CR33","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P.: E-matching with free variables. In: Voronkov, A., Bj\u00f8rner, N. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference, LPAR-18, LNCS, vol. 7180, pp. 359\u2013374. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28717-6_28"},{"key":"9352_CR34","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/978-3-642-18275-4_28","volume-title":"Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science","author":"P Suter","year":"2011","unstructured":"Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 6538, pp. 403\u2013418. Springer, Berlin (2011)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9352-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9352-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9352-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T12:03:38Z","timestamp":1567339418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9352-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,17]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["9352"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9352-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2015,11,17]]}}}