{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T02:24:35Z","timestamp":1763173475002,"version":"3.45.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["2204536"],"award-info":[{"award-number":["2204536"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1007\/s10270-024-01220-x","type":"journal-article","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T06:16:42Z","timestamp":1730096202000},"page":"1847-1868","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mutation testing for temporal alloy models (extended version)"],"prefix":"10.1007","volume":"24","author":[{"given":"Ana","family":"Jovanovic","sequence":"first","affiliation":[]},{"given":"Allison","family":"Sullivan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"key":"1220_CR1","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Lorber, F., Ni\u010dkovi\u0107, D.: Time for mutants-model-based mutation testing with timed automata. In: Tests and Proofs: 7th International Conference, TAP 2013, Budapest, Hungary, June 16-20, Proceedings 7. pp. 20\u201338. Springer (2013)","DOI":"10.1007\/978-3-642-38916-0_2"},{"key":"1220_CR2","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Salas, P.A.P.: Test case generation by OCL mutation and constraint solving. In: QSIC. pp. 64\u201371 (2005)","DOI":"10.1109\/QSIC.2005.63"},{"key":"1220_CR3","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":"1220_CR4","unstructured":"Alloy Grammer Reference: https:\/\/alloytools.org\/spec.html (2024)"},{"key":"1220_CR5","unstructured":"Alloy4Fun Benchmark: https:\/\/zenodo.org\/record\/4676413 (2022)"},{"key":"1220_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. In: Formal Aspects of Computing. pp.\u00a0544 (2018)","DOI":"10.1007\/s00165-017-0445-z"},{"issue":"1","key":"1220_CR7","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1002\/(SICI)1099-1689(199803)8:1<15::AID-STVR146>3.0.CO;2-D","volume":"8","author":"F Belli","year":"1998","unstructured":"Belli, F., Jack, O.: Declarative paradigm of test coverage. Softw. Test. Verif. Reliab. 8(1), 15\u201347 (1998)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"1220_CR8","doi-asserted-by":"crossref","unstructured":"Black, P.E., Okun, V., Yesha, Y.: Mutation of model checker specifications for test generation and evaluation. Mutation testing for the new century pp. 14\u201320 (2001)","DOI":"10.1007\/978-1-4757-5939-6_5"},{"key":"1220_CR9","unstructured":"Brida, S.G., Regis, G., Zheng, G., Bagheri, H., Nguyen, T., Aguirre, N., Frias, M.F.: Bounded exhaustive search of alloy specification repairs. In: ICSE (2021)"},{"key":"1220_CR10","doi-asserted-by":"publisher","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The electrum analyzer: model checking relational first-order temporal specifications. In: 2018 33rd IEEE\/ACM International Conference on Automated Software Engineering (ASE). pp. 884\u2013887 (2018). https:\/\/doi.org\/10.1145\/3238147.3240475","DOI":"10.1145\/3238147.3240475"},{"key":"1220_CR11","doi-asserted-by":"publisher","unstructured":"Carvalho, L., Degiovanni, R., Cordy, M., Aguirre, N., Le\u00a0Traon, Y., Papadakis, M.: Specbcfuzz: Fuzzing LTL solvers with boundary conditions. In: Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering. ICSE \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3597503.3639087,","DOI":"10.1145\/3597503.3639087"},{"key":"1220_CR12","doi-asserted-by":"crossref","unstructured":"Cerqueira, J., Cunha, A., Macedo, N.: Timely specification repair for alloy 6. In: Software Engineering and Formal Methods. pp. 288\u2013303 (2022)","DOI":"10.1007\/978-3-031-17108-6_18"},{"issue":"3","key":"1220_CR13","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10009-019-00540-4","volume":"22","author":"A Cunha","year":"2020","unstructured":"Cunha, A., Macedo, N.: Validating the hybrid ERTMS\/ETCS level 3 concept with electrum. Int. J. Softw. Tools Technol. Transf. 22(3), 281\u2013296 (2020)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"11","key":"1220_CR14","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/C-M.1978.218136","volume":"4","author":"RA DeMillo","year":"1978","unstructured":"DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Hints on test data selection: help for the practicing programmer. Computer 4(11), 34\u201341 (1978)","journal-title":"Computer"},{"key":"1220_CR15","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":"1220_CR16","volume-title":"ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications","author":"S Guti\u00e9rrez Brida","year":"2023","unstructured":"Guti\u00e9rrez Brida, S., Regis, G., Zheng, G., Bagheri, H., Nguyen, T., Aguirre, N., Frias, M.: ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications. Association for Computing Machinery, New York, NY, USA (2023)"},{"issue":"4","key":"1220_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/TSE.1977.231145","volume":"3","author":"RG Hamlet","year":"1977","unstructured":"Hamlet, R.G.: Testing programs with the aid of a compiler. IEEE Trans. Softw. Eng. 3(4), 279\u2013290 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.231145","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1220_CR18","volume-title":"Software abstractions: logic, language, and analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software abstractions: logic, language, and analysis. The MIT Press, USA (2006)"},{"issue":"5","key":"1220_CR19","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649\u2013678 (2011). https:\/\/doi.org\/10.1109\/TSE.2010.62","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1220_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"},{"issue":"2\u20133","key":"1220_CR21","first-page":"59","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The sat4j library, release 2.2. J. Satisf. Boolean Model. Comput. 7(2\u20133), 59\u201364 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"1220_CR22","doi-asserted-by":"crossref","unstructured":"Le, D., Alipour, M.A., Gopinath, R., Groce, A.: Mucheck: An extensible tool for mutation testing of haskell programs. In: Proceedings of the 2014 International Symposium on Software Testing and Analysis. pp. 429\u2013432 (2014)","DOI":"10.1145\/2610384.2628052"},{"key":"1220_CR23","doi-asserted-by":"crossref","unstructured":"Macedo, N., Cunha, A., Pereira, J., Carvalho, R., Silva, R., Paiva, A.C.R., Ramalho, M.S., Silva, D.: Experiences on teaching alloy with an automated assessment platform. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods. pp. 61\u201377 (2020)","DOI":"10.1007\/978-3-030-48077-6_5"},{"key":"1220_CR24","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: class diagrams analysis using alloy revisited. In: Models (2011)","DOI":"10.1007\/978-3-642-24485-8_44"},{"key":"1220_CR25","unstructured":"Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: ASE (2001)"},{"key":"1220_CR26","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: LISA (2010)"},{"key":"1220_CR27","unstructured":"Okun, V., Black, P.E., Yesha, Y.: Testing with model checker: insuring fault visibility. In: Proceedings of 2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems. pp. 1351\u20131356 (2003)"},{"key":"1220_CR28","doi-asserted-by":"crossref","unstructured":"Samimi, H., Aung, E.D., Millstein, T.D.: Falling back on executable specifications. In: ECOOP. pp. 552\u2013576 (2010)","DOI":"10.1007\/978-3-642-14107-2_26"},{"key":"1220_CR29","unstructured":"Software FDR2. http:\/\/www.fsel.com\/software.html"},{"issue":"53","key":"1220_CR30","first-page":"1","volume":"2005","author":"N Sorensson","year":"2005","unstructured":"Sorensson, N., Een, N.: Minisat v1. 13-a sat solver with conflict-clause minimization. SAT 2005(53), 1\u20132 (2005)","journal-title":"SAT"},{"key":"1220_CR31","unstructured":"Srivatanakul, T., Clark, J.A., Stepney, S., Polack, F.: Challenging formal specifications by mutation: a CSP security example. In: APSEC (2003)"},{"key":"1220_CR32","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":"1220_CR33","doi-asserted-by":"publisher","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), https:\/\/doi.org\/10.1145\/2632362.2632369","DOI":"10.1145\/2632362.2632369"},{"key":"1220_CR34","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":"1220_CR35","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":"1220_CR36","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":"1220_CR37","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":"1220_CR38","doi-asserted-by":"publisher","unstructured":"Wang, K., Sullivan, A., Marinov, D., Khurshid, S.: ASketch: a sketching framework for Alloy. In: 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ). pp. 121\u2013136 (2018).https:\/\/doi.org\/10.1007\/978-3-319-91271-4_9","DOI":"10.1007\/978-3-319-91271-4_9"},{"key":"1220_CR39","doi-asserted-by":"crossref","unstructured":"Zaeem, R.N., Khurshid, S.: Contract-based data structure repair using Alloy. In: ECOOP. pp. 577\u2013598 (2010)","DOI":"10.1007\/978-3-642-14107-2_27"},{"key":"1220_CR40","doi-asserted-by":"crossref","unstructured":"Zheng, G., Nguyen, T., Brida, S.G., Regis, G., Aguirre, N., Frias, M.F., Bagheri, H.: Atr: Template-based repair for alloy specifications. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. pp. 666\u2013677. ISSTA 2022 (2022)","DOI":"10.1145\/3533767.3534369"},{"key":"1220_CR41","doi-asserted-by":"crossref","unstructured":"Zheng, G., Nguyen, T., Guti\u00e9rrez\u00a0Brida, S., Regis, G., Frias, M.F., Aguirre, N., Bagheri, H.: 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":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01220-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01220-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01220-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T02:19:56Z","timestamp":1763173196000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01220-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"references-count":41,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["1220"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01220-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"30 April 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 July 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 October 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 October 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}