{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T13:37:45Z","timestamp":1771940265303,"version":"3.50.1"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,4,1]],"date-time":"2021-04-01T00:00:00Z","timestamp":1617235200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,4,1]],"date-time":"2021-04-01T00:00:00Z","timestamp":1617235200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["VRG11-005"],"award-info":[{"award-number":["VRG11-005"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004955","name":"\u00d6sterreichische Forschungsf\u00f6rderungsgesellschaft","doi-asserted-by":"publisher","award":["ECSEL JU under the project H2020 737469 AutoDrive"],"award-info":[{"award-number":["ECSEL JU under the project H2020 737469 AutoDrive"]}],"id":[{"id":"10.13039\/501100004955","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Austrian National Research Network S11403-N23 (RiS"],"award-info":[{"award-number":["Austrian National Research Network S11403-N23 (RiS"]}],"id":[{"id":"10.13039\/501100002428","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":[[2021,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a new method for model-based mutation-driven test case generation. Mutants are generated by making small syntactical modifications to the model or source code of the system under test. A test case kills a mutant if the behavior of the mutant deviates from the original system when running the test. In this work, we use hyperproperties\u2014which allow to express relations between multiple executions\u2014to formalize different notions of<jats:italic>killing<\/jats:italic>for both deterministic as well as non-deterministic models. The resulting hyperproperties are universal in the sense that they apply to arbitrary reactive models and mutants. Moreover, an off-the-shelf model checking tool for hyperproperties can be used to generate test cases. Furthermore, we propose solutions to overcome the limitations of current model checking tools via a model transformation and a bounded SMT encoding. We evaluate our approach on a number of models expressed in two different modeling languages by generating tests using a state-of-the-art mutation testing tool.<\/jats:p>","DOI":"10.1007\/s10270-020-00850-1","type":"journal-article","created":{"date-parts":[[2021,4,1]],"date-time":"2021-04-01T07:04:53Z","timestamp":1617260693000},"page":"405-427","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Mutation testing with hyperproperties"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3618-2251","authenticated-orcid":false,"given":"Andreas","family":"Fellner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mitra","family":"Tabaei\u00a0Befrouei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0143-632X","authenticated-orcid":false,"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,1]]},"reference":[{"key":"850_CR1","doi-asserted-by":"crossref","unstructured":"Aichernig, B., Brandl, H., J\u00f6bstl, E., Krenn, W., Schlick, R., Tiran, S.: MoMuT::UML model-based mutation testing for UML. In: 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST), ICST, pp. 1\u20138, April (2015)","DOI":"10.1002\/stvr.1522"},{"issue":"8","key":"850_CR2","doi-asserted-by":"publisher","first-page":"716","DOI":"10.1002\/stvr.1522","volume":"25","author":"BK Aichernig","year":"2015","unstructured":"Aichernig, B.K., Brandl, H., J\u00f6bstl, E., Krenn, W., Schlick, R., Tiran, S.: Killing strategies for model-based mutation testing. Softw. Test. Verif. Reliab. 25(8), 716\u2013748 (2015)","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"1\u20132","key":"850_CR3","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s00165-008-0083-6","volume":"21","author":"BK Aichernig","year":"2009","unstructured":"Aichernig, B.K., He, J.: Mutation testing in UTP. Formal Asp. Comput. 21(1\u20132), 33\u201364 (2009)","journal-title":"Formal Asp. Comput."},{"key":"850_CR4","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., J\u00f6bstl, E., Tiran, S.: Model-based mutation testing via symbolic refinement checking. (2014)","DOI":"10.1016\/j.scico.2014.05.004"},{"key":"850_CR5","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Lorber, F., Ni\u010dkovi\u0107, D.: Time for mutants\u2014model-based mutation testing with timed automata. In: International Conference on Tests and Proofs, pp. 20\u201338. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38916-0_2"},{"key":"850_CR6","doi-asserted-by":"crossref","unstructured":"Andrews, J.H., Briand, L.C., Labiche, Y.: Is mutation an appropriate tool for testing experiments? In Gruia-Catalin, R., Griswold W.G., Nuseibeh B. (eds.) 27th International Conference on Software Engineering (ICSE 2005), 15\u201321 May 2005, St. Louis, Missouri, USA, pp. 402\u2013411. ACM (2005)","DOI":"10.1145\/1062455.1062530"},{"issue":"5\u20137","key":"850_CR7","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1002\/stvr.1530","volume":"25","author":"P Arcaini","year":"2015","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Using mutation to assess fault detection capability of model review. Softw. Test. Verif. Reliab. 25(5\u20137), 629\u2013652 (2015)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"850_CR8","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Nuseen: a tool framework for the nusmv model checker. In: 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, March 13\u201317, 2017, pp. 476\u2013483. IEEE Computer Society (2017)"},{"key":"850_CR9","unstructured":"Bardin, S., Delahaye, M., David, R., Kosmatov, N., Papadakis, M., Traon, Y.L., Marion, J.-Y.: Sound and quasi-complete detection of infeasible test requirements. In: 8th IEEE International Conference on Software Testing, Verification and Validation, ICST 2015, Graz, Austria, April 13\u201317, 2015, pp. 1\u201310 (2015)"},{"key":"850_CR10","unstructured":"Bardin, S., Kosmatov, N., Cheynie, F.: Efficient leveraging of symbolic execution to advanced coverage criteria. In: Seventh IEEE International Conference on Software Testing, Verification and Validation, ICST 2014, March 31 2014\u2013April 4, 2014, Cleveland, Ohio, USA, pp. 173\u2013182 (2014)"},{"key":"850_CR11","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond, (2011). fmv.jku.at\/hwmcc11\/beyond1.pdf"},{"key":"850_CR12","unstructured":"Black, P.E., Okun, V., Yesha, Y.: Mutation operators for specifications. In: The Fifteenth IEEE International Conference on Automated Software Engineering, 2000. Proceedings ASE 2000, pp. 81\u201388. IEEE (2000)"},{"issue":"2","key":"850_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.08.002","volume":"190","author":"S Boroday","year":"2007","unstructured":"Boroday, S., Petrenko, A., Groz, R.: Can a model checker generate tests for non-deterministic systems? Electron. Notes Theor. Comput. Sci. 190(2), 3\u201319 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"850_CR14","doi-asserted-by":"crossref","unstructured":"Boroday, S., Petrenko, A., Groz, R., Quemener, Y.-M.: Test generation for CEFSM combining specification and fault coverage. In Schieferdecker, I., K\u00f6nig, H., Wolisz, A. (eds.) Testing of Communicating Systems XIV, Applications to Internet Technologies and Services, Proceedings of the IFIP 14th International Conference on Testing Communicating Systems - TestCom 2002, Berlin, Germany, March 19\u201322, 2002, volume 210 of IFIP Conference Proceedings, pp. 355\u2013372. Kluwer (2002)","DOI":"10.1007\/978-0-387-35497-2_25"},{"key":"850_CR15","doi-asserted-by":"crossref","unstructured":"Brett, N., Siddique, U., Bonakdarpour, B.: Rewriting-based runtime verification for alternation-free hyperltl. In Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22\u201329, 2017, Proceedings, Part II, volume 10206 of Lecture Notes in Computer Science, pp. 77\u201393 (2017)","DOI":"10.1007\/978-3-662-54580-5_5"},{"key":"850_CR16","doi-asserted-by":"crossref","unstructured":"Budd, T.A., Lipton, R.J., DeMillo, R.A., Sayward, F.G: Mutation analysis. Technical report, DTIC Document (1979)","DOI":"10.21236\/ADA068118"},{"key":"850_CR17","unstructured":"Cheng, S.-T., York, G., Brayton, R.K: Vl2mv: a compiler from verilog to blif-mv. HSIS Distribution, (1993)"},{"key":"850_CR18","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties, pp. 265\u2013284. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"850_CR19","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"850_CR20","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24\u201327, 2019, pp. 1\u201313. IEEE (2019)"},{"key":"850_CR21","doi-asserted-by":"crossref","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In Dillig I., Tasiran, S. (eds.) Computer aided verification - 31st international conference, CAV 2019, New York City, NY, USA, July 15\u201318, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pp. 121\u2013139. Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"850_CR22","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"4","key":"850_CR23","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/C-M.1978.218136","volume":"11","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. IEEE Comput. 11(4), 34\u201341 (1978)","journal-title":"IEEE Comput."},{"issue":"3","key":"850_CR24","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s10009-014-0355-9","volume":"18","author":"EP Enoiu","year":"2016","unstructured":"Enoiu, E.P., Causevic, A., Ostrand, T.J., Weyuker, E.J., Sundmark, D., Pettersson, P.: Automated test generation using model checking: an industrial evaluation. STTT 18(3), 335\u2013353 (2016)","journal-title":"STTT"},{"key":"850_CR25","doi-asserted-by":"crossref","unstructured":"Enoiu, E.P., Sundmark, D., Causevic, A., Feldt, R., Pettersson, P.: Mutation-based test generation for PLC embedded software using model checking. In: Wotawa, F., Nica, M., Kushik, N. (eds.) Testing Software and Systems\u201428th IFIP WG 6.1 International Conference, ICTSS 2016, Graz, Austria, October 17\u201319, 2016, Proceedings, volume 9976 of Lecture Notes in Computer Science, pp. 155\u2013171 (2016)","DOI":"10.1007\/978-3-319-47443-4_10"},{"key":"850_CR26","doi-asserted-by":"crossref","unstructured":"Fellner, A., Befrouei, M.T., Weissenbacher, G.: Mutation testing with hyperproperties. In: Csaba \u00d6lveczky, P., Sala\u00fcn, G. (eds.) Software Engineering and Formal Methods\u201417th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings, volume 11724 of Lecture Notes in Computer Science, pp. 203\u2013221. Springer (2019)","DOI":"10.1007\/978-3-030-30446-1_11"},{"key":"850_CR27","doi-asserted-by":"crossref","unstructured":"Fellner, A., Krenn, W., Schlick, R., Tarrach, T., Weissenbacher, G.: Model-based, mutation-driven test case generation via heuristic-guided branching search. In Talpin, J.-P. , Derler, P., Schneider, K. (eds.) Formal Methods and Models for System Design (MEMOCODE), pp. 56\u201366. ACM (2017)","DOI":"10.1145\/3127041.3127049"},{"key":"850_CR28","unstructured":"Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, August 23\u201326, 2016, Qu\u00e9bec City, Canada, volume\u00a059 of LIPIcs, pp. 13:1\u201313:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"key":"850_CR29","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M.: Eahyper: satisfiability, implication, and equivalence checking of hyperproperties. In CAV (2), volume 10427 of Lecture Notes in Computer Science, pp. 564\u2013570. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_29"},{"issue":"3","key":"850_CR30","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/s10703-019-00334-z","volume":"54","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Formal Methods Syst. Des. 54(3), 336\u2013363 (2019)","journal-title":"Formal Methods Syst. Des."},{"key":"850_CR31","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification (CAV), Lecture Notes in Computer Science, pp. 30\u201348. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"850_CR32","unstructured":"Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: STACS, volume\u00a066 of LIPIcs, pp. 30:1\u201330:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"850_CR33","unstructured":"Fraser, G., Gargantini, A.: An evaluation of model checkers for specification based test case generation. In: Second International Conference on Software Testing Verification and Validation, ICST 2009, Denver, Colorado, USA, April 1\u20134, 2009, pp. 41\u201350. IEEE Computer Society (2009)"},{"key":"850_CR34","doi-asserted-by":"crossref","unstructured":"Fraser, G., Wotawa, F.: Complementary criteria for testing temporal logic properties. In: Dubois, C. (ed.) Tests and Proofs, Third International Conference, TAP 2009, Zurich, Switzerland, July 2-3, 2009. Proceedings, volume 5668 of Lecture Notes in Computer Science, pp. 58\u201373. Springer (2009)","DOI":"10.1007\/978-3-642-02949-3_6"},{"issue":"3","key":"850_CR35","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1002\/stvr.402","volume":"19","author":"G Fraser","year":"2009","unstructured":"Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215\u2013261 (2009)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"850_CR36","doi-asserted-by":"crossref","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: ACM SIGSOFT Software Engineering Notes, vol. 24, pp. 146\u2013162. Springer, Berlin (1999)","DOI":"10.1145\/318774.318939"},{"issue":"4","key":"850_CR37","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. Software Eng. 3(4), 279\u2013290 (1977)","journal-title":"IEEE Trans. Software Eng."},{"key":"850_CR38","doi-asserted-by":"crossref","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 327\u2013341. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_23"},{"issue":"4","key":"850_CR39","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1109\/TSE.1982.235571","volume":"8","author":"WE Howden","year":"1982","unstructured":"Howden, W.E.: Weak mutation testing and completeness of test sets. IEEE Trans. Software Eng. 8(4), 371\u2013379 (1982)","journal-title":"IEEE Trans. Software Eng."},{"issue":"5","key":"850_CR40","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. Software Eng. 37(5), 649\u2013678 (2011)","journal-title":"IEEE Trans. Software Eng."},{"key":"850_CR41","doi-asserted-by":"crossref","unstructured":"Karimpour, J., Isazadeh, A., Noroozi, A.A.: Verifying observational determinism. In: Federrath H., Gollmann, D. (eds.) ICT Systems Security and Privacy Protection\u201430th IFIP TC 11 International Conference, SEC 2015, Hamburg, Germany, May 26-28, 2015, Proceedings, volume 455 of IFIP Advances in Information and Communication Technology, pp. 82\u201393. Springer (2015)","DOI":"10.1007\/978-3-319-18467-8_6"},{"key":"850_CR42","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina N., Veith, H. (eds.) Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pp. 1\u201335. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"issue":"1","key":"850_CR43","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des. 35(1), 73\u201397 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"850_CR44","unstructured":"Marcozzi, M.l., Delahaye, M.l., Bardin, S., Kosmatov, N., Prevosto, V.: Generic and effective specification of structural test objectives. In: 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, March 13\u201317, 2017, pp. 436\u2013441 (2017)"},{"issue":"1","key":"850_CR45","doi-asserted-by":"publisher","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J McLean","year":"1992","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37\u201358 (1992)","journal-title":"J. Comput. Secur."},{"key":"850_CR46","unstructured":"McMillan, K.L.: The SMV system. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)"},{"key":"850_CR47","unstructured":"Mutation testing with hyperproperies benchmark models. https:\/\/git-service.ait.ac.at\/sct-dse-public\/mutation-testing-with-hyperproperties. Uploaded: 2019-04-25"},{"issue":"4","key":"850_CR48","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G Nelson","year":"1989","unstructured":"Nelson, G.: A generalization of dijkstra\u2019s calculus. ACM Trans. Program. Lang. Syst. (TOPLAS) 11(4), 517\u2013561 (1989)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"1","key":"850_CR49","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/125489.125473","volume":"1","author":"OA Jefferson","year":"1992","unstructured":"Jefferson, O.A.: Investigations of the software testing coupling effect. ACM Trans. Softw. Eng. Methodol. 1(1), 5\u201320 (1992)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"850_CR50","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":"850_CR51","unstructured":"Rayadurgam, S., Per Erik, H., Mats: Coverage based test-case generation using model checkers. In Engineering of Computer Based Systems (ECBS), pp. 83\u201391. IEEE (2001)"},{"issue":"3","key":"850_CR52","first-page":"103","volume":"17","author":"J Tretmans","year":"1996","unstructured":"Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Softw. Concepts Tools 17(3), 103\u2013120 (1996)","journal-title":"Softw. Concepts Tools"},{"key":"850_CR53","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2006.11.002","volume":"168","author":"R van der Meyden","year":"2007","unstructured":"van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Electr. Notes Theor. Comput. Sci. 168, 61\u201375 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"4","key":"850_CR54","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1013886.1007526","volume":"29","author":"W Visser","year":"2004","unstructured":"Visser, W., P\u01ces\u01cereanu, C.S., Khurshid, S.: Test input generation with java pathfinder. ACM SIGSOFT Softw. Eng. Notes 29(4), 97\u2013107 (2004)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"850_CR55","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: Mualloy: a mutation testing framework for alloy. In International Conference on Software Engineering: Companion (ICSE-Companion), pp. 29\u201332. IEEE (2018)","DOI":"10.1145\/3183440.3183488"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00850-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00850-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00850-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,23]],"date-time":"2022-12-23T03:15:57Z","timestamp":1671765357000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00850-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["850"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00850-1","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4]]},"assertion":[{"value":"28 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 November 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 April 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}