{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T09:05:16Z","timestamp":1725613516208},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642242878"},{"type":"electronic","value":"9783642242885"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24288-5_11","type":"book-chapter","created":{"date-parts":[[2011,9,24]],"date-time":"2011-09-24T05:46:57Z","timestamp":1316843217000},"page":"110-124","source":"Crossref","is-referenced-by-count":2,"title":["Automated Termination in Model Checking Modulo Theories"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Carioni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_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, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"11_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., Henda, N.B., 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":"11_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: Proc. of LICS 2004, the 18th IEEE Int. Symp. on Logic in Computer Science (2004)","DOI":"10.1109\/LICS.2004.1319629"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-11266-9_1","volume-title":"SOFSEM 2010: Theory and Practice of Computer Science","author":"P.A. Abdulla","year":"2010","unstructured":"Abdulla, P.A.: Forcing monotonicity in parameterized verification: From multisets to words. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorn\u00fd, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol.\u00a05901, pp. 1\u201315. Springer, Heidelberg (2010)"},{"issue":"2","key":"11_CR5","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation\u00a0127(2), 91\u2013101 (1996)","journal-title":"Information and Computation"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theoretical Computer Science, 241\u2013264 (2003)","DOI":"10.1016\/S0304-3975(01)00330-9"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-15763-9_36","volume-title":"Distributed Computing","author":"F. Alberti","year":"2010","unstructured":"Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems\u2014a case study. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol.\u00a06343, pp. 392\u2013394. Springer, Heidelberg (2010)"},{"key":"11_CR8","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: Automated Termination in Model Checking Modulo Theories - extended version, http:\/\/homes.dsi.unimi.it\/~ghilardi\/allegati\/CGR_RP11_extended.pdf"},{"key":"11_CR9","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: MCMT in the Land of Parametrized Timed Automata. In: Proc. of VERIFY 2010 (2010)"},{"key":"11_CR10","volume-title":"Model Theory","author":"C.-C. Chang","year":"1990","unstructured":"Chang, C.-C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland, Amsterdam (1990)","edition":"3"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-48168-0_5","volume-title":"Computer Science Logic","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 50\u201366. Springer, Heidelberg (1999)"},{"key":"11_CR12","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)"},{"key":"11_CR13","first-page":"352","volume-title":"Proc. of LICS","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. of LICS, pp. 352\u2013359. IEEE Computer Society, Los Alamitos (1999)"},{"key":"11_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-71070-7_6","volume-title":"Automated Reasoning","author":"S. Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT Model-Checking of Array-based Systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 67\u201382. Springer, Heidelberg (2008)"},{"key":"11_CR15","unstructured":"Ghilardi, S., Ranise, S.: A Note on the Stopping Failures Models, Unpublished Draft, mcmt web site (2009)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-02716-1_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Ghilardi","year":"2009","unstructured":"Ghilardi, S., Ranise, S.: Goal Directed Invariant Synthesis for Model Checking Modulo Theories. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol.\u00a05607, pp. 173\u2013188. Springer, Heidelberg (2009)"},{"key":"11_CR17","unstructured":"Ghilardi, S., Ranise, S.: Model Checking Modulo Theory at work: the integration of Yices in MCMT. In: AFM 2009 (co-located with CAV 2009) (2009)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT-solving: termination and invariant synthesis. LMCS\u00a06(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"11_CR19","unstructured":"Ghilardi, S., Ranise, S., Valsecchi, T.: Light-Weight SMT-based Model-Checking. In: Proc. of AVOCS 2007-2008, ENTCS (2008)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S. Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A Model Checker Modulo Theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 22\u201329. Springer, Heidelberg (2010)"},{"issue":"5","key":"11_CR21","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","volume":"83","author":"S. Philippe","year":"2002","unstructured":"Philippe, S.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters\u00a083(5), 251\u2013261 (2002)","journal-title":"Information Processing Letters"},{"key":"11_CR22","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, Dep. of Comp. Science, Iowa (2006), http:\/\/www.SMT-LIB.org\/papers"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24288-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T10:00:14Z","timestamp":1560679214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24288-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642242878","9783642242885"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24288-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}