{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T12:12:16Z","timestamp":1781007136002,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_55","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"718-724","source":"Crossref","is-referenced-by-count":59,"title":["Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Conchon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amit","family":"Goel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sava","family":"Krsti\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alain","family":"Mebsout","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fatiha","family":"Za\u00efdi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"55_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"55_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 (On Efficient Verification of Parameterized Systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 721\u2013736. Springer, Heidelberg (2007)"},{"key":"55_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":"55_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Ro\u010dkai, P.: DiVinE: Parallel Distributed Model Checker (Tool paper). In: HiBi\/PDMC, pp. 4\u20137 (2010)","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"key":"55_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-47813-2_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Baukus","year":"2002","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 317\u2013330. Springer, Heidelberg (2002)"},{"key":"55_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"issue":"2","key":"55_CR7","first-page":"51","volume":"198","author":"S. Conchon","year":"2008","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): Semantic combination of congruence closure with solvable theories. ENTCS\u00a0198(2), 51\u201369 (2008)","journal-title":"ENTCS"},{"key":"55_CR8","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: ICCD, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"55_CR9","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Kalyanasundaram, K.: Functory: A distributed computing library for Objective Caml. In: TFP, pp. 65\u201381 (2011)","DOI":"10.1007\/978-3-642-32037-8_5"},{"key":"55_CR10","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: IJCAR, pp. 67\u201382 (2008)","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"55_CR11","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":"55_CR12","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: IJCAR, pp. 22\u201329 (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"55_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/11560548_12","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 129\u2013145. Springer, Heidelberg (2005)"},{"issue":"1","key":"55_CR14","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/s10009-008-0094-x","volume":"11","author":"I. Melatti","year":"2009","unstructured":"Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.: Parallel and distributed model checking in Eddy. STTT\u00a011(1), 13\u201325 (2009)","journal-title":"STTT"},{"key":"55_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/3-540-61474-5_78","volume-title":"Computer Aided Verification","author":"S. Park","year":"1996","unstructured":"Park, S., Dill, D.L.: Protocol Verification by Aggregation of Distributed Transactions. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 300\u2013310. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_55.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T09:30:31Z","timestamp":1743586231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}