{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T12:09:13Z","timestamp":1725970153533},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319779348"},{"type":"electronic","value":"9783319779355"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_29","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T15:02:34Z","timestamp":1520694154000},"page":"435-451","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Execution and Reachability Analysis Using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion"],"prefix":"10.1007","author":[{"given":"Miguel","family":"Romero","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Camilo","family":"Rocha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"issue":"2","key":"29_CR1","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"G Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213\u2013239 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"29_CR2","unstructured":"Barco, A., Knight, S., Valencia, F.D.: K-Stores: a spatial and epistemic concurrent constraint interpreter. In: 21st Workshop on Functional and Constraint Logic Programming (WFLP2012), Nagoya, Japan. Informal Proceedings (2012)"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","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.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"29_CR4","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1016\/j.entcs.2004.06.019","volume":"117","author":"C Braga","year":"2005","unstructured":"Braga, C., Meseguer, J.: Modular rewriting semantics in practice. Electron. Notes Theor. Comput. Sci. 117, 393\u2013416 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20133","key":"29_CR5","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Caccamo, M., Buttazzo, G., Sha, L.: Capacity sharing for overrun control. In: 21st IEEE Real-Time Systems Symposium, pp. 295\u2013304. IEEE (2000)","DOI":"10.1109\/REAL.2000.896018"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All about Maude - a High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic","year":"2007","unstructured":"Clavel, M. (ed.): All about Maude - a High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. Lecture Notes in Computer Science, vol. 4350. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"issue":"1\u20132","key":"29_CR8","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/S0304-3975(01)00165-7","volume":"275","author":"P Degano","year":"2002","unstructured":"Degano, P., Gadducci, F., Priami, C.: A causal semantics for CCS via rewriting logic. Theor. Comput. Sci. 275(1\u20132), 259\u2013282 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-642-24933-4_17","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"F Dur\u00e1n","year":"2011","unstructured":"Dur\u00e1n, F., Rocha, C., \u00c1lvarez, J.M.: Towards a Maude formal environment. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 329\u2013351. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24933-4_17"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"29_CR11","unstructured":"Estlin, T., Jonsson, A., Pasareanu, C., Simmons, R., Tso, K., Verma, V.: Plan execution interchange language (PLEXIL). Technical report TM-2006-213483, NASA, April 2006"},{"key":"29_CR12","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/j.scico.2014.07.003","volume":"99","author":"R Guti\u00e9rrez","year":"2015","unstructured":"Guti\u00e9rrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. Sci. Comput. Program. 99, 235\u2013261 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"29_CR13","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/j.jlamp.2016.09.001","volume":"86","author":"M Guzm\u00e1n","year":"2017","unstructured":"Guzm\u00e1n, M., Haar, S., Perchy, S., Rueda, C., Valencia, F.D.: Belief, knowledge, lies and other utterances in an algebra for space and extrusion. J. Log. Algebr. Methods Program. 86(1), 107\u2013133 (2017)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"29_CR14","unstructured":"Guzm\u00e1n, M., Valencia, F.D., Herbstritt, M.: On the expressiveness of spatial constraint systems. Technical report, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern\/Saarbruecken, Germany (2016)"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-32940-1_23","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"S Knight","year":"2012","unstructured":"Knight, S., Palamidessi, C., Panangaden, P., Valencia, F.D.: Spatial and epistemic modalities in constraint-based process calculi. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 317\u2013332. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_23"},{"issue":"1","key":"29_CR16","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR17","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1016\/j.ic.2013.08.004","volume":"231","author":"J Meseguer","year":"2013","unstructured":"Meseguer, J., Ro\u015fu, G.: The rewriting logic semantics project: a progress report. Inf. Comput. 231, 38\u201369 (2013)","journal-title":"Inf. Comput."},{"key":"29_CR18","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/S1571-0661(05)80134-3","volume":"36","author":"P \u00d6lveczky","year":"2000","unstructured":"\u00d6lveczky, P., Meseguer, J.: Real-time maude: a tool for simulating and analyzing real-time and hybrid systems. Electron. Notes Theor. Comput. Sci. 36, 361\u2013382 (2000)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"29_CR19","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebr. Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"29_CR20","unstructured":"Romero, M.: Una sem\u00e1ntica ejecutable en l\u00f3gica de reescritura para programaci\u00f3n espacial concurrente por restricciones (SCCP). Trabajo de grado 001\/522, Escuela Colombiana de Ingenieria Julio Garavito, Bogot\u00e1, Colombia, January 2017"},{"key":"29_CR21","unstructured":"Romero, M., Rocha, C.: Reachability analysis for spatial concurrent constraint systems with extrusion (2017). http:\/\/camilorocha.info\/publications"},{"key":"29_CR22","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2086.001.0001","volume-title":"Concurrent Constraint Programming. Logic programming","author":"V Saraswat","year":"1993","unstructured":"Saraswat, V.: Concurrent Constraint Programming. Logic programming. MIT Press, Cambridge (1993)"},{"issue":"1\u20132","key":"29_CR23","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s10703-005-2254-x","volume":"27","author":"A Verdejo","year":"2005","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Formal Methods Syst. Des. 27(1\u20132), 113\u2013172 (2005)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"29_CR24","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285(2), 487\u2013517 (2002)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,12]],"date-time":"2019-10-12T17:02:07Z","timestamp":1570899727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}