{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:58:51Z","timestamp":1779087531967,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540710691","type":"print"},{"value":"9783540710707","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_6","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"67-82","source":"Crossref","is-referenced-by-count":37,"title":["Towards SMT Model Checking of Array-Based Systems"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrica","family":"Nicolini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniele","family":"Zucchelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite state systems. In: Proc. of LICS 1996, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-540-71209-1_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Regular model checking without transducers. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 721\u2013736. Springer, Heidelberg (2007)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-73368-3_17","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 145\u2013157. Springer, Heidelberg (2007)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74240-1_1","volume-title":"Fundamentals of Computation Theory","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In: Csuhaj-Varj\u00fa, E., \u00c9sik, Z. (eds.) FCT 2007. LNCS, vol.\u00a04639, pp. 1\u201322. Springer, Heidelberg (2007)"},{"issue":"10","key":"6_CR5","doi-asserted-by":"publisher","first-page":"1493","DOI":"10.1016\/j.ic.2005.05.011","volume":"204","author":"M. Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient theory combination via boolean search. Information and Computation\u00a0204(10), 1493\u20131525 (2006)","journal-title":"Information and Computation"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"6_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L.M. Moura de","year":"2002","unstructured":"de Moura, L.M., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"6_CR8","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, London (1972)"},{"issue":"3","key":"6_CR9","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10009-005-0193-x","volume":"8","author":"Y. Fang","year":"2006","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. Software Tools for Technology\u00a08(3), 261\u2013279 (2006)","journal-title":"Software Tools for Technology"},{"key":"6_CR10","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. Technical Report RI318-08, Universit\u00e0 degli Studi di Milano (2008), http:\/\/homes.dsi.unimi.it\/~zucchell\/publications\/techreport\/GhiNiRaZu-RI318-08.pdf"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Proc. of TACAS 2008","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Proc. of TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y. Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theoretical Computer Science\u00a0256(1-2), 93\u2013112 (2001)","journal-title":"Theoretical Computer Science"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/93385.93442","volume-title":"Proc. of PODC 1990","author":"Z. Manna","year":"1990","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proc. of PODC 1990, pp. 377\u2013410. ACM Press, New York (1990)"},{"issue":"6","key":"6_CR14","doi-asserted-by":"publisher","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. Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-540-39866-0_24","volume-title":"Perspectives of System Informatics","author":"T. Rybina","year":"2004","unstructured":"Rybina, T., Voronkov, A.: A logical reconstruction of reachability. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol.\u00a02890, pp. 222\u2013237. Springer, Heidelberg (2004)"},{"key":"6_CR16","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation\u00a03, 141\u2013224 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:15:16Z","timestamp":1605762916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}