{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:57:50Z","timestamp":1743055070348,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031314759"},{"type":"electronic","value":"9783031314766"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-31476-6_8","type":"book-chapter","created":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T07:02:46Z","timestamp":1684220566000},"page":"151-169","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The Role of\u00a0Abstraction in\u00a0Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3481-5307","authenticated-orcid":false,"given":"Mar\u00eda-del-Mar","family":"Gallardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2456-4946","authenticated-orcid":false,"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6399-6162","authenticated-orcid":false,"given":"Laura","family":"Panizo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,17]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jss.2013.10.056","volume":"90","author":"D Adalid","year":"2014","unstructured":"Adalid, D., Salmer\u00f3n, A., Gallardo, M., Merino, P.: Using SPIN for automated debugging of infinite executions of java programs. J. Syst. Softw. 90, 61\u201375 (2014). https:\/\/doi.org\/10.1016\/j.jss.2013.10.056","journal-title":"J. Syst. Softw."},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Bosnacki, D.: Enhancing state space reduction techniques for model checking. Ph.D. thesis, Department of Mathematics and Computer Science (2001). https:\/\/doi.org\/10.6100\/IR549628","DOI":"10.6100\/IR549628"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1002\/stvr.422","volume":"21","author":"P de la C\u00e1mara","year":"2011","unstructured":"de la C\u00e1mara, P., Castro, J.R., Gallardo, M., Merino, P.: Verification support for ARINC-653-based avionics software. Softw. Test. Verif. Reliab. 21(4), 267\u2013298 (2011). https:\/\/doi.org\/10.1002\/stvr.422","journal-title":"Softw. Test. Verif. Reliab."},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11691617_11","volume-title":"Model Checking Software","author":"P de la C\u00e1mara","year":"2006","unstructured":"de la C\u00e1mara, P., del Mar Gallardo, M., Merino, P.: Abstract matching for software model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 182\u2013200. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691617_11"},{"issue":"5","key":"8_CR5","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/s10009-009-0112-7","volume":"11","author":"P de la C\u00e1mara","year":"2009","unstructured":"de la C\u00e1mara, P., Gallardo, M., Merino, P., San\u00e1n, D.: Checking the reliability of socket based communication software. Int. J. Softw. Tools Technol. Transf. 11(5), 359\u2013374 (2009). https:\/\/doi.org\/10.1007\/s10009-009-0112-7","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR6","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from java source code. In: Ghezzi, C., Jazayeri, M., Wolf, A.L. (eds.) Proceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, 4\u201311 June 2000, pp. 439\u2013448. ACM (2000). https:\/\/doi.org\/10.1145\/337180.337234","DOI":"10.1145\/337180.337234"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1155\/2017\/2012696","volume":"2017","author":"AR Espada","year":"2017","unstructured":"Espada, A.R., Gallardo, M., Salmer\u00f3n, A., Merino, P.: Performance analysis of spotify\u00ae for android with model-based testing. Mob. Inf. Syst. 2017, 67\u201377 (2017). https:\/\/doi.org\/10.1155\/2017\/2012696","journal-title":"Mob. Inf. Syst."},{"issue":"4\u20135","key":"8_CR9","doi-asserted-by":"publisher","first-page":"e1699","DOI":"10.1002\/stvr.1699","volume":"29","author":"AR Espada","year":"2019","unstructured":"Espada, A.R., Gallardo, M., Salmer\u00f3n, A., Panizo, L., Merino, P.: A formal approach to automatically analyse extra-functional properties in mobile applications. Softw. Test. Verification Reliab. 29(4\u20135), e1699 (2019). https:\/\/doi.org\/10.1002\/stvr.1699","journal-title":"Softw. Test. Verification Reliab."},{"issue":"2\u20133","key":"8_CR10","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s10009-003-0122-9","volume":"5","author":"MM Gallardo","year":"2004","unstructured":"Gallardo, M.M., Mart\u00ednez, J., Merino, P., Pimentel, E.: aSPIN: a tool for abstract model checking. Softw. Tools Technol. Transf. 5(2\u20133), 165\u2013184 (2004)","journal-title":"Softw. Tools Technol. Transf."},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-04570-7_20","volume-title":"Formal Methods for Industrial Critical Systems","author":"MM Gallardo","year":"2009","unstructured":"Gallardo, M.M., Merino, P., Panizo, L., Linares, A.: Developing a decision support tool for dam management with SPIN. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 210\u2013212. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04570-7_20"},{"issue":"11","key":"8_CR12","doi-asserted-by":"publisher","first-page":"1329","DOI":"10.1002\/spe.1048","volume":"41","author":"MM Gallardo","year":"2011","unstructured":"Gallardo, M.M., Merino, P., Panizo, L., Linares, A.: A practical use of model checking for synthesis: generating a dam controller for flood management. Softw. Pract. Exp. 41(11), 1329\u20131347 (2011)","journal-title":"Softw. Pract. Exp."},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45789-5_28","volume-title":"Static Analysis","author":"MM Gallardo","year":"2002","unstructured":"Gallardo, M.M., Merino, P., Pimentel, E.: Refinement of LTL formulas for abstract model checking. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 395\u2013410. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45789-5_28"},{"issue":"3","key":"8_CR14","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/s00165-004-0040-y","volume":"16","author":"MM Gallardo","year":"2004","unstructured":"Gallardo, M.M., Merino, P., Pimentel, E.: A generalized semantics of PROMELA for abstract model checking. Formal Aspects Comput. 16(3), 166\u2013193 (2004)","journal-title":"Formal Aspects Comput."},{"issue":"2\u20134","key":"8_CR15","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-009-9124-y","volume":"42","author":"MM Gallardo","year":"2009","unstructured":"Gallardo, M.M., Merino, P., San\u00e1n, D.: Model checking dynamic memory allocation in operating systems. J. Autom. Reasoning 42(2\u20134), 229\u2013264 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"8_CR16","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1016\/j.scico.2011.10.003","volume":"77","author":"M Gallardo","year":"2012","unstructured":"Gallardo, M., Joubert, C., Merino, P., San\u00e1n, D.: A model-extraction approach to verifying concurrent C programs with CADP. Sci. Comput. Program. 77(3), 375\u2013392 (2012). https:\/\/doi.org\/10.1016\/j.scico.2011.10.003","journal-title":"Sci. Comput. Program."},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-030-30985-5_32","volume-title":"From Software Engineering to Formal Methods and Tools, and Back","author":"M\u2013M Gallardo","year":"2019","unstructured":"Gallardo, M.\u2013M., Luque-Schempp, F., Merino-G\u00f3mez, P., Panizo, L.: How formal methods can contribute to 5G networks. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 548\u2013571. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30985-5_32"},{"issue":"6","key":"8_CR18","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1002\/stvr.1505","volume":"24","author":"M Gallardo","year":"2014","unstructured":"Gallardo, M., Panizo, L.: Extending model checkers for hybrid system verification: the case study of SPIN. Softw. Test. Verif. Reliab. 24(6), 438\u2013471 (2014). https:\/\/doi.org\/10.1002\/stvr.1505","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"4","key":"8_CR19","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/s10515-012-0113-8","volume":"20","author":"M Gallardo","year":"2013","unstructured":"Gallardo, M., San\u00e1n, D.: Verification of complex dynamic data tree with mu-calculus. Autom. Softw. Eng. 20(4), 569\u2013612 (2013). https:\/\/doi.org\/10.1007\/s10515-012-0113-8","journal-title":"Autom. Softw. Eng."},{"issue":"4","key":"8_CR20","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA pathfinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000). https:\/\/doi.org\/10.1007\/s100090050043","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"5","key":"8_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR22","volume-title":"The SPIN Model Checker : Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN Model Checker\u202f: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Holzmann, G. J., Joshi, R.: Model-driven software verification. In: Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, 1-3 April 2004. Proceedings 11, pp. 76-91. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/b96721","DOI":"10.1007\/b96721"},{"issue":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1002\/stvr.228","volume":"11","author":"GJ Holzmann","year":"2001","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verification Reliab. 11(2), 65\u201379 (2001)","journal-title":"Softw. Test. Verification Reliab."},{"key":"8_CR25","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1998","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin (1998)"},{"issue":"6","key":"8_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2382756.2382793","volume":"37","author":"L Panizo","year":"2012","unstructured":"Panizo, L., Gallardo, M.: An extension of Java PathFinder for hybrid systems. ACM SIGSOFT Softw. Eng. Notes 37(6), 1\u20135 (2012)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"issue":"1","key":"8_CR27","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1177\/0037549714557054","volume":"91","author":"A Salmer\u00f3n","year":"2015","unstructured":"Salmer\u00f3n, A., Merino, P.: Integrating model checking and simulation for protocol optimization. SIMULATION 91(1), 3\u201325 (2015). https:\/\/doi.org\/10.1177\/0037549714557054","journal-title":"SIMULATION"}],"container-title":["Lecture Notes in Computer Science","Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-31476-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T07:04:07Z","timestamp":1684220647000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-31476-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031314759","9783031314766"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-31476-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 May 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}