{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:07:11Z","timestamp":1742965631222,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192369"},{"type":"electronic","value":"9783319192376"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19237-6_30","type":"book-chapter","created":{"date-parts":[[2015,5,26]],"date-time":"2015-05-26T13:15:31Z","timestamp":1432646131000},"page":"479-488","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Applying Predicate Abstraction to Abstract State Machines"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Bianchi","sequence":"first","affiliation":[]},{"given":"Sebastiano","family":"Pizzutilo","sequence":"additional","affiliation":[]},{"given":"Gennaro","family":"Vessio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,5,27]]},"reference":[{"key":"30_CR1","unstructured":"Agrawal, D.P., Zeng, Q.A.: Introduction to Wireless and Mobile Systems. Thomson Brooks\/Cole (2003)"},{"issue":"4","key":"30_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining Liveness. Information Processing Letters 21(4), 181\u2013185 (1985)","journal-title":"Information Processing Letters"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-11811-1_6","volume-title":"Abstract State Machines, Alloy, B and Z","author":"P Arcaini","year":"2010","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 61\u201374. Springer, Heidelberg (2010)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-642-29860-8_17","volume-title":"Runtime Verification","author":"P Arcaini","year":"2012","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: conformance monitoring of java programs by abstract state machines. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 223\u2013238. Springer, Heidelberg (2012)"},{"key":"30_CR5","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Chacking. The MIT Press (2008)"},{"issue":"3","key":"30_CR6","first-page":"295","volume":"37","author":"A Bianchi","year":"2013","unstructured":"Bianchi, A., Manelli, L., Pizzutilo, S.: An ASM-based Model for Grid Job Management. Informatica (Slovenia) 37(3), 295\u2013306 (2013)","journal-title":"Informatica (Slovenia)"},{"key":"30_CR7","first-page":"29","volume":"1","author":"A Bianchi","year":"2014","unstructured":"Bianchi, A., Pizzutilo, S., Vessio, G.: Suitability of Abstract State Machines for Discussing Mobile Ad-hoc Networks. Global Journal of Advanced Software Engineering 1, 29\u201338 (2014)","journal-title":"Global Journal of Advanced Software Engineering"},{"issue":"4","key":"30_CR8","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1145\/937555.937561","volume":"4","author":"A Blass","year":"2003","unstructured":"Blass, A., Gurevich, Y.: Abstract State Machines Capture Parallel Algorithms. ACM Transactions on Computational Logic 4(4), 578\u2013651 (2003)","journal-title":"ACM Transactions on Computational Logic"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"30_CR10","unstructured":"Chen, Z., Zhou, C., Ding, D.: Automatic abstraction refinement for petri nets verification. In: 10th Int. Workshop on High-Level Design, Validation and Test, pp. 168\u2013174 (2005)"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Dershowitz, N.: The Generic Model of Computation. Electronic Proceedings in Theoretical Computer Science (2013)","DOI":"10.4204\/EPTCS.88.5"},{"issue":"2","key":"30_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"EW Dijkstra","year":"1971","unstructured":"Dijkstra, E.W.: Hierarchical Ordering of Sequential Processes. ACTA Informatica 1(2), 115\u2013138 (1971)","journal-title":"ACTA Informatica"},{"key":"30_CR14","unstructured":"Farahbod, R., Gl\u00e4sser, U., Ma, G.: Model checking CoreASM specifications. In: 14th International ASM Workshop (2007)"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Gabrisch, W.: A hoare-style verification calculus for control state ASMs. In: 5th Balkan Conference on Informatics, pp. 205\u2013210 (2012)","DOI":"10.1145\/2371316.2371357"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-36498-6_15","volume-title":"Abstract State Machines 2003. Advances in Theory and Practice","author":"A Gargantini","year":"2003","unstructured":"Gargantini, A., Riccobene, E., Rinzivillo, S.: Using spin to generate testsfrom ASM specifications. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 263\u2013277. Springer, Heidelberg (2003)"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-30885-7_6","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"V Gervasi","year":"2012","unstructured":"Gervasi, V.: An ASM model of concurrency in a web browser. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 79\u201393. Springer, Heidelberg (2012)"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-11447-2_4","volume-title":"Rigorous Methods for Software Construction and Analysis","author":"A Glausch","year":"2009","unstructured":"Glausch, A., Reisig, W.: An ASM-characterization of a class of distributed algorithms. In: Abrial, J.-R., Gl\u00e4sser, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 50\u201364. Springer, Heidelberg (2009)"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"1","key":"30_CR20","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/343369.343384","volume":"1","author":"Y Gurevich","year":"2000","unstructured":"Gurevich, Y.: Sequential Abstract State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic 1(1), 77\u2013111 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"30_CR21","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley (1979)"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-30793-5_5","volume-title":"Formal Techniques for Distributed Systems","author":"K Klai","year":"2012","unstructured":"Klai, K., Desel, J.: Checking soundness of business processes compositionally using symbolic observation graphs. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE 2012. LNCS, vol. 7273, pp. 67\u201383. Springer, Heidelberg (2012)"},{"key":"30_CR23","first-page":"268","volume":"53","author":"E Kindler","year":"1994","unstructured":"Kindler, E.: Safety and Liveness Properties: A Survey. EATCS Bulletin 53, 268\u2013272 (1994)","journal-title":"EATCS Bulletin"},{"key":"30_CR24","unstructured":"Laplante, P.: Dictionary of Computer Science. Engineering and Technology. CRC Press (2000)"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-30885-7_25","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"A Luzzana","year":"2012","unstructured":"Luzzana, A., Rossetti, M., Righettini, P., Scandurra, P.: Modeling synchronization\/communication patterns in vision-based robot control applications using ASMs. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 331\u2013335. Springer, Heidelberg (2012)"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Belding-Royer, E.M., Das, S.R.: Ad hoc On-Demand Distance Vector (AODV) Routing. RFC 3561 (2003). http:\/\/tools.ietf.org\/html\/rfc3561","DOI":"10.17487\/rfc3561"},{"key":"30_CR27","first-page":"209","volume":"22","author":"W Reisig","year":"2003","unstructured":"Reisig, W.: The Expressive Power of Abstract State Machines. Computing and Informatics 22, 209\u2013219 (2003)","journal-title":"Computing and Informatics"},{"issue":"11","key":"30_CR28","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/2.43525","volume":"22","author":"M Singhal","year":"1989","unstructured":"Singhal, M.: Deadlock Detection in Distributed Systems. IEEE Computer 22(11), 37\u201348 (1989)","journal-title":"IEEE Computer"},{"key":"30_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/3-540-48683-6_37","volume-title":"Computer Aided Verification","author":"M Spielmann","year":"1999","unstructured":"Spielmann, M.: Automatic verification of abstract state machines. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 431\u2013442. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Business Information Processing","Enterprise, Business-Process and Information Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19237-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T12:04:13Z","timestamp":1675857853000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19237-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192369","9783319192376"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19237-6_30","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 May 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}