{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:16:49Z","timestamp":1785543409873,"version":"3.56.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031637896","type":"print"},{"value":"9783031637902","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-63790-2_9","type":"book-chapter","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T14:03:41Z","timestamp":1718892221000},"page":"141-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Analysis of\u00a0the\u00a0Impact of\u00a0Field-Value Instance Navigation in\u00a0Alloy\u2019s Model Finding"],"prefix":"10.1007","author":[{"given":"C\u00e9sar","family":"Cornejo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mar\u00eda Marta","family":"Novaira","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sonia","family":"Permigiani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcelo","family":"Frias","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sim\u00f3n Guti\u00e9rrez","family":"Brida","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Germ\u00e1n","family":"Regis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,6,21]]},"reference":[{"key":"9_CR1","unstructured":"Replication package. https:\/\/sites.google.com\/view\/field-value-evaluation"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Abad, P., et al.: Improving test generation under rich contracts by tight bounds and incremental SAT solving. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, 18\u201322 March 2013, pp. 21\u201330. IEEE Computer Society (2013)","DOI":"10.1109\/ICST.2013.46"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Alhanahnah, M., Stevens, C., Bagheri, H.: Scalable analysis of interaction threats in IoT systems. In: Khurshid, S., Pasareanu, C.S. (eds.) ISSTA 2020: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, USA, 18\u201322 July 2020, pp. 272\u2013285. ACM (2020)","DOI":"10.1145\/3395363.3397347"},{"issue":"5","key":"9_CR4","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/s00165-017-0445-z","volume":"30","author":"H Bagheri","year":"2018","unstructured":"Bagheri, H., Kang, E., Malek, S., Jackson, D.: A formal approach for detection of security flaws in the android permission system. Formal Aspects Comput. 30(5), 525\u2013544 (2018)","journal-title":"Formal Aspects Comput."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bagheri, H., Sadeghi, A., Behrouz, R.J., Malek, S.: Practical, formal synthesis and automatic enforcement of security policies for android. In: 46th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2016, Toulouse, France, 28 June\u20131 July 2016, pp. 514\u2013525. IEEE Computer Society (2016)","DOI":"10.1109\/DSN.2016.53"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The electrum analyzer: model checking relational first-order temporal specifications. In: Huchard, M., K\u00e4stner, C., Fraser, G. (eds.) Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, 3\u20137 September 2018, pp. 884\u2013887. ACM (2018)","DOI":"10.1145\/3238147.3240475"},{"key":"9_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd edn. MIT Press, Cambridge (2018)","edition":"2"},{"issue":"4","key":"9_CR8","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-66197-1_11","volume-title":"Software Engineering and Formal Methods","author":"N Danas","year":"2017","unstructured":"Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 168\u2013184. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_11"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F.S.-H., Jackson, D.: Modular verification of code with SAT. In: Pollock, L.L., Pezz\u00e8, M. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, 17\u201320 July 2006, pp. 109\u2013120. ACM (2006)","DOI":"10.1145\/1146238.1146251"},{"issue":"OOPSLA1","key":"9_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3527323","volume":"6","author":"T Dyer","year":"2022","unstructured":"Dyer, T., Nelson, T., Fisler, K., Krishnamurthi, S.: Applying cognitive principles to model-finding output: the positive value of negative information. Proc. ACM Program. Lang. 6(OOPSLA1), 1\u201329 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252\u2013265. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_25"},{"issue":"9","key":"9_CR13","doi-asserted-by":"publisher","first-page":"1283","DOI":"10.1109\/TSE.2013.15","volume":"39","author":"JP Galeotti","year":"2013","unstructured":"Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: efficient sat-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283\u20131307 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., Pombo, C.L., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Tonella, P., Orso, A. (edis.) Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, Trento, Italy, 12\u201316 July 2010, pp. 25\u201336. ACM (2010)","DOI":"10.1145\/1831708.1831712"},{"key":"9_CR15","unstructured":"Ghezzi, C., Jazayeri, M., Mandrioli, D.: Fundamentals of Software Engineering, 2nd edn. Prentice Hall (2003)"},{"issue":"1 &2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0743-1066(93)90018-C","volume":"15","author":"JN Hooker","year":"1993","unstructured":"Hooker, J.N.: Solving the incremental satisfiability problem. J. Log. Program. 15(1 &2), 177\u2013186 (1993)","journal-title":"J. Log. Program."},{"issue":"2","key":"9_CR17","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9_CR18","volume-title":"Software Abstractions - Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"issue":"9","key":"9_CR19","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019)","journal-title":"Commun. ACM"},{"issue":"2","key":"9_CR20","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1145\/276393.276396","volume":"20","author":"D Jackson","year":"1998","unstructured":"Jackson, D., Jha, S., Damon, C.: Isomorph-free model enumeration: a new method for checking relational specifications. ACM Trans. Program. Lang. Syst. 20(2), 302\u2013343 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the alloy constraint analyzer. 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. 730\u2013733. ACM (2000)","DOI":"10.1145\/337180.337616"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Jovanovic, A., Sullivan, A.: REACH: refining alloy scenarios by size (tools and artifact track). In: IEEE 33rd International Symposium on Software Reliability Engineering, ISSRE 2022, Charlotte, NC, USA, 31 October\u20133 November 2022, pp. 229\u2013238. IEEE (2022)","DOI":"10.1109\/ISSRE55969.2022.00031"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Khalek, S.A., Yang, G., Zhang, L., Marinov, D., Khurshid, S.: TestEra: a tool for testing java programs using alloy specifications. In: Alexander, P., Pasareanu, C.S., Hosking, J.G. (eds.) 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2011), Lawrence, KS, USA, 6\u201310 November 2011, pp. 608\u2013611. IEEE Computer Society (2011)","DOI":"10.1109\/ASE.2011.6100137"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, 13\u201318 November 2016, pp. 373\u2013383. ACM (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-662-46675-9_20","volume-title":"Fundamental Approaches to Software Engineering","author":"N Macedo","year":"2015","unstructured":"Macedo, N., Cunha, A., Guimar\u00e3es, T.: Exploring scenario exploration. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 301\u2013315. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_20"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"102690","DOI":"10.1016\/j.scico.2021.102690","volume":"211","author":"N Macedo","year":"2021","unstructured":"Macedo, N., et al.: Experiences on teaching alloy with an automated assessment platform. Sci. Comput. Program. 211, 102690 (2021)","journal-title":"Sci. Comput. Program."},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Mansoor, N., Bagheri, H., Kang, E., Sharif, B.: An empirical study assessing software modeling in alloy. In: 11th IEEE\/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2023, Melbourne, Australia, 14\u201315 May 2023, pp. 44\u201354. IEEE (2023)","DOI":"10.1109\/FormaliSE58978.2023.00013"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Mirzaei, N., Garcia, J., Bagheri, H., Sadeghi, A., Malek, S.: Reducing combinatorics in GUI testing of android applications. In: Dillon, L.K., Visser, W., Williams, L.A. (eds.) Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, 14\u201322 May 2016, pp. 559\u2013570. ACM (2016)","DOI":"10.1145\/2884781.2884853"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-662-54494-5_2","volume-title":"Fundamental Approaches to Software Engineering","author":"V Montaghami","year":"2017","unstructured":"Montaghami, V., Rayside, D.: Bordeaux: a tool for thinking outside the box. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 22\u201339. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54494-5_2"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Nelson, T., Danas, N., Dougherty, D.J., Krishnamurthi, S.: The power of \u201cwhy\u201d and \u201cwhy not\u201d: enriching scenario exploration with provenance. In: Bodden, E., Sch\u00e4fer, W., van Deursen, A., Zisman, A. (eds.) Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017, Paderborn, Germany, 4\u20138 September 2017, pp. 106\u2013116. ACM (2017)","DOI":"10.1145\/3106237.3106272"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE 2013, San Francisco, CA, USA, 18\u201326 May 2013, pp. 232\u2013241. IEEE Computer Society (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-031-27481-7_21","volume-title":"Formal Methods","author":"JO Ringert","year":"2023","unstructured":"Ringert, J.O., Sullivan, A.: Abstract alloy instances. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 364\u2013382. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_21"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Sullivan, A.: Hawkeye: user-guided enumeration of scenarios. In: Jin, Z., et al. (eds.) 32nd IEEE International Symposium on Software Reliability Engineering, ISSRE 2021, Wuhan, China, 25\u201328 October 2021, pp. 569\u2013578. IEEE (2021)","DOI":"10.1109\/ISSRE52982.2021.00064"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: Automated model repair for alloy. In: Huchard, M., K\u00e4stner, C., Fraser, G. (eds.) Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, 3\u20137 September 2018, pp. 577\u2013588. ACM (2018)","DOI":"10.1145\/3238147.3238162"},{"issue":"12","key":"9_CR35","doi-asserted-by":"publisher","first-page":"1144","DOI":"10.1109\/TSE.2017.2655056","volume":"43","author":"P Zave","year":"2017","unstructured":"Zave, P.: Reasoning about identifier spaces: how to make chord correct. IEEE Trans. Softw. Eng. 43(12), 1144\u20131156 (2017)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-36675-8_5","volume-title":"Automated Reasoning and Mathematics","author":"H Zhang","year":"2013","unstructured":"Zhang, H., Zhang, J.: MACE4 and SEM: a comparison of finite model generators. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 101\u2013130. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_5"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63790-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T08:49:13Z","timestamp":1732265353000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63790-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031637896","9783031637902"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63790-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"21 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author(s) has no competing interests to declare that are relevant to the content of this manuscript.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergamo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}