{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T05:58:54Z","timestamp":1769925534157,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287558","type":"print"},{"value":"9783642287565","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_34","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"478-484","source":"Crossref","is-referenced-by-count":8,"title":["McScM: A General Framework for the Verification of Communicating Machines"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Heu\u00dfner","sequence":"first","affiliation":[]},{"given":"Tristan","family":"Le Gall","sequence":"additional","affiliation":[]},{"given":"Gr\u00e9goire","family":"Sutre","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"34_CR1","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"P. Aziz Abdulla","year":"1996","unstructured":"Aziz Abdulla, P., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation\u00a0130(1), 71\u201390 (1996)","journal-title":"Information and Computation"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 372\u2013386. Springer, Heidelberg (2004)"},{"issue":"2","key":"34_CR3","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On Communicating Finite-State Machines. J. ACM\u00a030(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"issue":"5","key":"34_CR4","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Renement for Symbolic Model Checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"34_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1042038.1042039","volume":"6","author":"T. Henzinger","year":"2005","unstructured":"Henzinger, T., Majumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Transactions on Computational Logic\u00a06, 1\u201332 (2005)","journal-title":"ACM Transactions on Computational Logic"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Heu\u00dfner, A., Le Gall, T., Sutre, G.: Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol.\u00a05578, pp. 107\u2013124. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02652-2_11"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-21461-5_13","volume-title":"Formal Techniques for Distributed Systems","author":"G. Kalyon","year":"2011","unstructured":"Kalyon, G., Le Gall, T., Marchand, H., Massart, T.: Global State Estimates for Distributed Systems. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol.\u00a06722, pp. 198\u2013212. Springer, Heidelberg (2011)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/11784180_17","volume-title":"Algebraic Methodology and Software Technology","author":"T. Gall Le","year":"2006","unstructured":"Le Gall, T., Jeannet, B., J\u00e9ron, T.: Verification of Communication Protocols Using Abstract Interpretation of FIFO Queues. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 204\u2013219. Springer, Heidelberg (2006)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"34_CR10","unstructured":"CADP, \n                    \n                      http:\/\/www.inrialpes.fr\/vasy\/cadp\/"},{"key":"34_CR11","unstructured":"LASH, \n                    \n                      http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"34_CR12","unstructured":"LEVER, \n                    \n                      http:\/\/abhayspace.com\/static\/lever.html"},{"key":"34_CR13","unstructured":"LTSA, \n                    \n                      http:\/\/www.doc.ic.ac.uk\/ltsa\/"},{"key":"34_CR14","unstructured":"McScM, \n                    \n                      https:\/\/altarica.labri.fr\/forge\/projects\/mcscm"},{"key":"34_CR15","unstructured":"SCM, Lattice Automata, \n                    \n                      http:\/\/gforge.inria.fr\/projects\/bjeannet\/"},{"key":"34_CR16","unstructured":"SPIN, \n                    \n                      http:\/\/spinroot.com"},{"key":"34_CR17","unstructured":"TaPAS, \n                    \n                      http:\/\/altarica.labri.fr\/forge\/projects\/3\/wiki\/TaPAS\/"},{"key":"34_CR18","unstructured":"TReX, \n                    \n                      http:\/\/www.liafa.jussieu.fr\/~sighirea\/trex\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T23:59:25Z","timestamp":1556495965000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}