{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T23:31:12Z","timestamp":1756683072981,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031773815"},{"type":"electronic","value":"9783031773822"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-77382-2_18","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:11Z","timestamp":1732562771000},"page":"309-327","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Right or\u00a0Wrong \u2013 Understanding How Users Write Software Models in\u00a0Alloy"],"prefix":"10.1007","author":[{"given":"Ana","family":"Jovanovic","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7400-2218","authenticated-orcid":false,"given":"Allison","family":"Sullivan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Akhawe, D., Barth, A., Lam, P.E., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: 2010 23rd IEEE Computer Security Foundations Symposium, pp. 290\u2013304 (2010)","DOI":"10.1109\/CSF.2010.27"},{"key":"18_CR2","unstructured":"Alloy analyzer Website (2019). http:\/\/alloytools.org"},{"key":"18_CR3","unstructured":"Alloy Grammar Reference (2024). https:\/\/alloytools.org\/spec.html"},{"key":"18_CR4","unstructured":"Alloy4Fun Benchmark (2022). https:\/\/zenodo.org\/record\/4676413"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-57663-9_1","volume-title":"Frontiers in Software Engineering Education","author":"M Askarpour","year":"2020","unstructured":"Askarpour, M., Bersani, M.M.: Teaching formal methods: an experience report. In: Bruel, J.-M., Capozucca, A., Mazzara, M., Meyer, B., Naumchev, A., Sadovykh, A. (eds.) FISEE 2019. LNCS, vol. 12271, pp. 3\u201318. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57663-9_1"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bagheri, H., Kang, E., Malek, S., Jackson, D.: A formal approach for detection of security flaws in the Android permission system. Formal Asp. Comput. (2018)","DOI":"10.1007\/s00165-017-0445-z"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Bagheri, H., Malek, S.: Titanium: efficient analysis of evolving alloy specifications. In: Proceedings of the 2016 24th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pp. 27\u201338 (2016)","DOI":"10.1145\/2950290.2950337"},{"key":"18_CR8","unstructured":"Boyatt, R., Sinclair, J.: Experiences of teaching a lightweight formal method (2008)"},{"key":"18_CR9","unstructured":"Brida, S.G., et al.: Bounded exhaustive search of alloy specification repairs. In: ICSE (2021)"},{"key":"18_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-031-17108-6_18","volume-title":"SEFM 2022","author":"J Cerqueira","year":"2022","unstructured":"Cerqueira, J., Cunha, A., Macedo, N.: Timely specification repair for alloy 6. In: Schlingloff, B.H., Chai, M. (eds.) SEFM 2022. LNCS, vol. 13550, pp. 288\u2013303. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_18"},{"issue":"4","key":"18_CR11","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/3296979.3192373","volume":"53","author":"N Chong","year":"2018","unstructured":"Chong, N., Sorensen, T., Wickerson, J.: The semantics of transactions and weak memory in x86, Power, ARM, and C++. SIGPLAN Not. 53(4), 211\u2013225 (2018)","journal-title":"SIGPLAN Not."},{"key":"18_CR12","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"},{"issue":"OOPSLA1","key":"18_CR13","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":"18_CR14","doi-asserted-by":"crossref","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. TSE (2013)","DOI":"10.1109\/TSE.2013.15"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-19835-9_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Gopinath","year":"2011","unstructured":"Gopinath, D., Malik, M.Z., Khurshid, S.: Specification-based program repair using SAT. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 173\u2013188. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_15"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Guti\u00e9rrez Brida, S., et al.: ICEBAR: feedback-driven iterative repair of alloy specifications. Association for Computing Machinery, New York, NY, USA (2023)","DOI":"10.1145\/3551349.3556944"},{"key":"18_CR17","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA, August 2000","DOI":"10.1145\/347324.383378"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Jovanovic, A., Sullivan, A.: Reach: refining alloy scenarios by size (tools and artifact track). In: 2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE), pp. 229\u2013238 (2022)","DOI":"10.1109\/ISSRE55969.2022.00031"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Jovanovic, A., Sullivan, A.: Mutation testing for temporal alloy models. In: 26th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS, pp. 228\u2013238 (2023)","DOI":"10.1109\/MODELS58315.2023.00013"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-30942-8_1","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"S Krishnamurthi","year":"2019","unstructured":"Krishnamurthi, S., Nelson, T.: The human in formal methods. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 3\u201310. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_1"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-030-48077-6_5","volume-title":"Rigorous State-Based Methods","author":"N Macedo","year":"2020","unstructured":"Macedo, N., et al.: Experiences on teaching alloy with an automated assessment platform. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 61\u201377. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_5"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Mansoor, N., Bagheri, H., Kang, E., Sharif., B.: An empirical study assessing software modeling in alloy. In: International Conference on Formal Methods in Software Engineering, pp. 44\u201354 (2023)","DOI":"10.1109\/FormaliSE58978.2023.00013"},{"key":"18_CR24","unstructured":"Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: ASE (2001)"},{"key":"18_CR25","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: LISA (2010)"},{"key":"18_CR26","unstructured":"Simonot, M.: Teaching abstraction in mathematics and computer science - a computer-supported approach with alloy (2012)"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for alloy. In: ICST (2017)","DOI":"10.1109\/ICST.2017.31"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Sullivan, A., Zaeem, R.N., Khurshid, S., Marinov, D.: Towards a test automation framework for alloy. In: Proceedings of the 2014 SPIN Workshop on Software Model Checking, pp. 113\u2013116 (2014). http:\/\/doi.acm.org.ncat.idm.oclc.org\/10.1145\/2632362.2632369","DOI":"10.1145\/2632362.2632369"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Trippel, C., Lustig, D., Martonosi, M.: Security verification via automatic hardware-aware exploit synthesis: The CheckMate Approach. IEEE Micro (2019)","DOI":"10.1109\/MM.2019.2910010"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: Automated model repair for Alloy. In: ASE (2018)","DOI":"10.1145\/3238147.3238162"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: MuAlloy: a mutation testing framework for alloy. In: Proceedings of the 40th International Conference on Software Engineering (ICSE) Demo Track, pp. 29\u201332 (2018). https:\/\/doi.org\/10.1145\/3183440.3183488","DOI":"10.1145\/3183440.3183488"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: Fault localization for declarative models in Alloy. In: ISSRE (2020)","DOI":"10.1109\/ISSRE5003.2020.00044"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-030-17462-0_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Wang","year":"2019","unstructured":"Wang, W., Wang, K., Gligoric, M., Khurshid, S.: Incremental analysis of evolving alloy models. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 174\u2013191. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_10"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: POPL (2017)","DOI":"10.1145\/3009837.3009838"},{"key":"18_CR35","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"},{"key":"18_CR36","unstructured":"Zave, P.: How to make Chord correct (using a stable base). CoRR abs\/1502.06461 (2015)"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"Zheng, G., Bagheri, H., Rothermel, G., Wang, J.: Platinum: reusing constraint solutions in bounded analysis of relational logic. In: International Conference on Fundamental Approaches to Software Engineering (2020)","DOI":"10.1007\/978-3-030-45234-6_2"},{"key":"18_CR38","doi-asserted-by":"crossref","unstructured":"Zheng, G., et al.: ATR: template-based repair for alloy specifications. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2022. pp. 666\u2013677 (2022)","DOI":"10.1145\/3533767.3534369"},{"key":"18_CR39","doi-asserted-by":"crossref","unstructured":"Zheng, G., et al.: Flack: counterexample-guided fault localization for alloy models. In: 2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE), pp. 637\u2013648 (2021)","DOI":"10.1109\/ICSE43902.2021.00065"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T20:03:15Z","timestamp":1732564995000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}