{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:25:31Z","timestamp":1769732731829,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031274800","type":"print"},{"value":"9783031274817","type":"electronic"}],"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-27481-7_21","type":"book-chapter","created":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T14:03:10Z","timestamp":1677765790000},"page":"364-382","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Abstract Alloy Instances"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3610-3920","authenticated-orcid":false,"given":"Jan Oliver","family":"Ringert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7400-2218","authenticated-orcid":false,"given":"Allison","family":"Sullivan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,3,3]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Akhawe, D., Barth, A., Lam, P.E., Mitchell, J.C., Song, D.: Towards a formal foundation of web security. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, 17\u201319 July 2010, pp. 290\u2013304. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/CSF.2010.27","DOI":"10.1109\/CSF.2010.27"},{"key":"21_CR2","unstructured":"Alloy: Alloy Tools GitHub. https:\/\/github.com\/AlloyTools (2022). Accessed 5 2022"},{"key":"21_CR3","unstructured":"Alloy 6 Language Reference. https:\/\/alloytools.org\/spec.html (2022). Accessed 8 2022"},{"issue":"1","key":"21_CR4","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K Anastasakis","year":"2010","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to alloy. Softw. Syst. Model. 9(1), 69\u201386 (2010). https:\/\/doi.org\/10.1007\/s10270-008-0110-3","journal-title":"Softw. Syst. Model."},{"issue":"1","key":"21_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10270-013-0353-5","volume":"14","author":"A Cunha","year":"2013","unstructured":"Cunha, A., Garis, A., Riesco, D.: Translating between Alloy specifications and UML class diagrams annotated with OCL. Softw. Syst. Model. 14(1), 5\u201325 (2013). https:\/\/doi.org\/10.1007\/s10270-013-0353-5","journal-title":"Softw. Syst. Model."},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Dini, N., Yelen, C., Alrmaih, Z., Kulkarni, A., Khurshid, S.: Korat-API: a framework to enhance Korat to better support testing and reliability techniques. In: SAC (2018)","DOI":"10.1145\/3167132.3167339"},{"key":"21_CR7","doi-asserted-by":"publisher","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(OOPSLA), 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3527323","DOI":"10.1145\/3527323"},{"issue":"2","key":"21_CR8","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":"21_CR9","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":"21_CR10","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). https:\/\/doi.org\/10.1145\/3338843","journal-title":"Commun. ACM"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-24605-3_21","volume-title":"Theory and Applications of Satisfiability Testing","author":"S Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A case for efficient solution enumeration. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 272\u2013286. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_21"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-24485-8_44","volume-title":"Model Driven Engineering Languages and Systems","author":"S Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: class diagrams analysis using alloy revisited. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 592\u2013607. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24485-8_44"},{"key":"21_CR13","unstructured":"Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: ASE (2001)"},{"key":"21_CR14","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3106237.3106272","DOI":"10.1145\/3106237.3106272"},{"key":"21_CR15","doi-asserted-by":"publisher","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\u201913, San Francisco, CA, USA, 18\u201326 May 2013, pp. 232\u2013241. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/ICSE.2013.6606569","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"21_CR16","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: LISA (2010)"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Ponzio, P., Aguirre, N., Frias, M.F., Visser, W.: Field-exhaustive testing. In: FSE (2016)","DOI":"10.1145\/2950290.2950336"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-319-95582-7_34","volume-title":"Formal Methods","author":"S Porncharoenwase","year":"2018","unstructured":"Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 568\u2013587. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_34"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Ringert, J.O., Sullivan, A.K.: Abstract alloy instances artefact (2022). https:\/\/doi.org\/10.5281\/zenodo.7339931","DOI":"10.5281\/zenodo.7339931"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Ringert, J.O., Sullivan, A.K.: Abstract alloy instances code (2022). https:\/\/github.com\/jringert\/alloy-absinst","DOI":"10.1007\/978-3-031-27481-7_21"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-642-14107-2_26","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"H Samimi","year":"2010","unstructured":"Samimi, H., Aung, E.D., Millstein, T.: Falling back on executable specifications. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 552\u2013576. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_26"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. In: SAT (2001)","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Sullivan, A.: Hawkeye: user-guided enumeration of scenarios. In: Jin, Z., Li, X., Xiang, J., Mariani, L., Liu, T., Yu, X., Ivaki, N. (eds.) 32nd IEEE International Symposium on Software Reliability Engineering, ISSRE 2021, Wuhan, China, 25\u201328 October 2021, pp. 569\u2013578. IEEE (2021). https:\/\/doi.org\/10.1109\/ISSRE52982.2021.00064","DOI":"10.1109\/ISSRE52982.2021.00064"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Sullivan, A.: Hawkeye: user guided enumeration of scenarios. In: ISSRE (2021)","DOI":"10.1109\/ISSRE52982.2021.00064"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Jovanovic, A.: Reach: refining alloy scenarios by size. In: ISSRE (2022)","DOI":"10.1109\/ISSRE55969.2022.00031"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-32409-4_21","volume-title":"Formal Methods and Software Engineering","author":"A Sullivan","year":"2019","unstructured":"Sullivan, A., Marinov, D., Khurshid, S.: Solution enumeration abstraction: a modeling idiom to enhance a lightweight formal method. In: Ait-Ameur, Y., Qin, S. (eds.) ICFEM 2019. LNCS, vol. 11852, pp. 336\u2013352. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32409-4_21"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for alloy. In: 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, 13\u201317 March 2017, pp. 264\u2013275. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ICST.2017.31","DOI":"10.1109\/ICST.2017.31"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"},{"issue":"3","key":"21_CR29","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/MM.2019.2910010","volume":"39","author":"C Trippel","year":"2019","unstructured":"Trippel, C., Lustig, D., Martonosi, M.: Security verification via automatic hardware-aware exploit synthesis: the CheckMate approach. IEEE Micro 39(3), 84\u201393 (2019)","journal-title":"IEEE Micro"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/978-3-642-14107-2_27","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"R Nokhbeh Zaeem","year":"2010","unstructured":"Nokhbeh Zaeem, R., Khurshid, S.: Contract-based data structure repair using alloy. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 577\u2013598. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_27"},{"issue":"12","key":"21_CR31","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). https:\/\/doi.org\/10.1109\/TSE.2017.2655056","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"21_CR32","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Soft. Eng. 28(2), 183\u2013200 (2002). https:\/\/doi.org\/10.1109\/32.988498","journal-title":"IEEE Trans. Soft. Eng."},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Zhang, C., et al.: Alloymax: bringing maximum satisfaction to relational specifications. In: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 155\u2013167. ESEC\/FSE 2021, Association for Computing Machinery, New York, NY, USA (2021)","DOI":"10.1145\/3468264.3468587"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-27481-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,27]],"date-time":"2023-03-27T05:54:11Z","timestamp":1679896451000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-27481-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031274800","9783031274817"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-27481-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 March 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"L\u00fcbeck","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 March 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 March 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fm2023.isp.uni-luebeck.de\/wordpress\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"95","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also include 7 short industry papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}