{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:32Z","timestamp":1749318092640},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415901"},{"type":"electronic","value":"9783319415918"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-41591-8_17","type":"book-chapter","created":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T17:27:27Z","timestamp":1466702847000},"page":"253-269","source":"Crossref","is-referenced-by-count":14,"title":["SMT-Based Automatic Proof of ASM Model Refinement"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"issue":"2","key":"17_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"17_CR2","first-page":"1","volume":"77","author":"J-R Abrial","year":"2007","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundam. Inform. 77(1), 1\u201328 (2007)","journal-title":"Fundam. Inform."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: Proceedings of MEMOCODE 2015, pp. 80\u201389. IEEE (2015)","DOI":"10.1109\/MEMCOD.2015.7340473"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-33600-8_29","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Mashkoor","year":"2016","unstructured":"Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329\u2013343. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-33600-8_29"},{"key":"17_CR5","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Using SMT for dealing with nondeterminism in ASM-based runtime verification. In: ECEASST, vol. 70 (2014)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Rigorous development process of a safety-critical system: from ASM models to Java code. Int. J. Softw. Tools Technol. Transf. 1\u201323 (2015)","DOI":"10.1007\/s10009-015-0394-x"},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1002\/spe.1019","volume":"41","author":"P Arcaini","year":"2011","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Experience 41, 155\u2013166 (2011)","journal-title":"Softw. Pract. Experience"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Holom, R.-M., Riccobene, E.: ASM-based formal design of an adaptivity component for a cloud system. Formal Aspects Comput. 1\u201329 (2016)","DOI":"10.1007\/s00165-016-0371-5"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0027231","volume-title":"Formal Methods for Industrial Applications","author":"C Beierle","year":"1996","unstructured":"Beierle, C., B\u00f6rger, E., Durdanovi\u0107, I., Gl\u00e4sser, U., Riccobene, E.: Refining abstract machine specifications of the steam boiler control to well documented executable code. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165, pp. 52\u201378. Springer, Heidelberg (1996)"},{"issue":"2","key":"17_CR10","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s00165-012-0266-z","volume":"26","author":"EA Boiten","year":"2012","unstructured":"Boiten, E.A.: Introducing extra operations in refinement. Formal Aspects Comput. 26(2), 305\u2013317 (2012)","journal-title":"Formal Aspects Comput."},{"key":"17_CR11","series-title":"Communications in Computer and Information Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-07512-9_1","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"F Boniol","year":"2014","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1\u201318. Springer, Heidelberg (2014)"},{"issue":"2","key":"17_CR12","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/s00165-003-0012-7","volume":"15","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM refinement method. Formal Aspects Comput. 15(2), 237\u2013257 (2003)","journal-title":"Formal Aspects Comput."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E.: The Abstract State Machines method for high-level system design and analysis. In: Formal Methods: State of the Art and New Directions, pp. 79\u2013116. Springer, London (2010)","DOI":"10.1007\/978-1-84882-736-3_3"},{"key":"17_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"17_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0257-1","volume-title":"Refinement in Z and object-Z: Foundations and Advanced Applications","author":"J Derrick","year":"2001","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and object-Z: Foundations and Advanced Applications. Springer, London (2001)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-662-43652-3_16","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"G Ernst","year":"2014","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Modular refinement for submachines of ASMs. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 188\u2013203. Springer, Heidelberg (2014)"},{"issue":"2","key":"17_CR17","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1002\/spe.1029","volume":"41","author":"R Farahbod","year":"2011","unstructured":"Farahbod, R., Gl\u00e4sser, U.: The CoreASM modeling framework. Softw. Pract. Experience 41(2), 167\u2013178 (2011)","journal-title":"Softw. Pract. Experience"},{"key":"17_CR18","first-page":"219","volume":"2","author":"NA Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Q. 2, 219\u2013246 (1989)","journal-title":"CWI Q."},{"issue":"2","key":"17_CR19","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"NA Lynch","year":"1995","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: Part I. untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995)","journal-title":"Inf. Comput."},{"issue":"2","key":"17_CR20","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.jlap.2009.07.003","volume":"79","author":"J Meseguer","year":"2010","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Algebraic simulations. J. Logic Algebraic Program. 79(2), 103\u2013143 (2010)","journal-title":"J. Logic Algebraic Program."},{"issue":"7","key":"17_CR21","first-page":"597","volume":"6","author":"E Riccobene","year":"2000","unstructured":"Riccobene, E., Schmid, J.: Capturing requirements by abstract state machines: The light control case study. J. UCS 6(7), 597\u2013620 (2000)","journal-title":"J. UCS"},{"issue":"11","key":"17_CR22","first-page":"952","volume":"7","author":"G Schellhorn","year":"2001","unstructured":"Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. J. UCS 7(11), 952\u2013979 (2001)","journal-title":"J. UCS"},{"issue":"12","key":"17_CR23","first-page":"1929","volume":"14","author":"G Schellhorn","year":"2008","unstructured":"Schellhorn, G.: ASM refinement preserving invariants. J. UCS 14(12), 1929\u20131948 (2008)","journal-title":"J. UCS"},{"key":"17_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine","author":"R St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine, vol. 24. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41591-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:57:27Z","timestamp":1498323447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41591-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415901","9783319415918"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41591-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}