{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:23:59Z","timestamp":1770279839418,"version":"3.49.0"},"reference-count":95,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T00:00:00Z","timestamp":1531267200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T00:00:00Z","timestamp":1531267200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-1217824"],"award-info":[{"award-number":["CCF-1217824"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-1054786"],"award-info":[{"award-number":["CCF-1054786"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s10515-018-0240-y","type":"journal-article","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T15:10:39Z","timestamp":1531321839000},"page":"917-960","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["How verified (or tested) is my code? Falsification-driven verification and testing"],"prefix":"10.1007","volume":"25","author":[{"given":"Alex","family":"Groce","sequence":"first","affiliation":[]},{"given":"Iftekhar","family":"Ahmed","sequence":"additional","affiliation":[]},{"given":"Carlos","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Paul E.","family":"McKenney","sequence":"additional","affiliation":[]},{"given":"Josie","family":"Holmes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,11]]},"reference":[{"key":"240_CR1","doi-asserted-by":"publisher","unstructured":"Ahmed, I., Gopinath, R., Brindescu, C., Groce, A., Jensen, C.: Can testedness be effectively measured? In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, pp. 547\u2013558. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2950290.2950324","DOI":"10.1145\/2950290.2950324"},{"key":"240_CR2","doi-asserted-by":"crossref","unstructured":"Ahmed, I., Jensen, C., Groce, A., McKenney, P.E.: Applying mutation analysis on kernel test suites: an experience report. In: International Workshop on Mutation Analysis, pp. 110\u2013115 (2017)","DOI":"10.1109\/ICSTW.2017.26"},{"key":"240_CR3","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K.: Model-based mutation testing of reactive systems. In: Theories of Programming and Formal Methods, pp. 23\u201336. Springer (2013)","DOI":"10.1007\/978-3-642-39698-4_2"},{"key":"240_CR4","unstructured":"Alipour, M.A., Groce, A., Zhang, C., Sanadaji, A., Caushik, G.: Finding model-checkable needles in large source code haystacks: Modular bug-finding via static analysis and dynamic invariant discovery. In: International Workshop on Constraints in Formal Verification (2013)"},{"key":"240_CR5","doi-asserted-by":"crossref","unstructured":"Andrews, J.H., Briand, L.C., Labiche, Y.: Is mutation an appropriate tool for testing experiments? In: International Conference on Software Engineering, pp. 402\u2013411 (2005)","DOI":"10.1145\/1062455.1062530"},{"key":"240_CR6","doi-asserted-by":"crossref","unstructured":"Andrews, J.H., Groce, A., Weston, M., Xu, R.G.: Random test run length and effectiveness. In: Automated Software Engineering, pp. 19\u201328 (2008)","DOI":"10.1109\/ASE.2008.12"},{"issue":"8","key":"240_CR7","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1109\/TSE.2006.83","volume":"32","author":"JH Andrews","year":"2006","unstructured":"Andrews, J.H., Briand, L.C., Labiche, Y., Namin, A.S.: Using mutation analysis for assessing and comparing testing coverage criteria. IEEE Trans. Softw. Eng. 32(8), 608 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"240_CR8","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1002\/stvr.1486","volume":"24","author":"A Arcuri","year":"2014","unstructured":"Arcuri, A., Briand, L.: A hitchhiker\u2019s guide to statistical tests for assessing randomized algorithms in software engineering. Softw. Test. Verif. Reliab. 24(3), 219\u2013250 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"240_CR9","unstructured":"Auerbach, G., Copty, F., Paruthi, V.: Formal verification of arbiters using property strengthening and underapproximations. In: Formal Methods in Computer-Aided Design, pp. 21\u201324 (2010)"},{"key":"240_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11513988_8","volume-title":"Computer Aided Verification","author":"Thomas Ball","year":"2005","unstructured":"Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: Computer Aided Verification, pp. 67\u201381 (2005)"},{"issue":"5","key":"240_CR11","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1109\/TSE.2014.2372785","volume":"41","author":"ET Barr","year":"2015","unstructured":"Barr, E.T., Harman, M., McMinn, P., Shahbaz, M., Yoo, S.: The oracle problem in software testing: a survey. IEEE Trans. Softw. Eng. 41(5), 507\u2013525 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"12","key":"240_CR12","doi-asserted-by":"publisher","first-page":"1040","DOI":"10.1145\/358476.358484","volume":"26","author":"J Bentley","year":"1983","unstructured":"Bentley, J.: Programming pearls: writing correct programs. Commun. ACM 26(12), 1040\u20131045 (1983)","journal-title":"Commun. ACM"},{"key":"240_CR13","first-page":"14","volume":"2000","author":"PE Black","year":"2000","unstructured":"Black, P.E., Okun, V., Yesha, Y.: Mutation of model checker specifications for test generation and evaluation. Mutation 2000, 14\u201320 (2000)","journal-title":"Mutation"},{"key":"240_CR14","unstructured":"Bloch, J.: Extra, extra - read all about it: nearly all binary searches and mergesorts are broken. http:\/\/googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html (2006)"},{"key":"240_CR15","unstructured":"bremen, mrbean, jmcgeheeiv, et\u00a0al.: pyfakefs implements a fake file system that mocks the Python file system modules. https:\/\/github.com\/jmcgeheeiv\/pyfakefs (2011)"},{"key":"240_CR16","doi-asserted-by":"crossref","unstructured":"Budd, T.A., DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Theoretical and empirical studies on using program mutation to test the functional correctness of programs. In: Principles of Programming Languages, pp. 220\u2013233. ACM (1980)","DOI":"10.21236\/ADA083078"},{"key":"240_CR17","unstructured":"Budd, T.A.: Mutation analysis of program test data. Ph.D. thesis, Yale University, New Haven, CT, USA (1980)"},{"key":"240_CR18","doi-asserted-by":"publisher","DOI":"10.21236\/ADA068118","volume-title":"Mutation Analysis","author":"TA Budd","year":"1979","unstructured":"Budd, T.A., Lipton, R.J., DeMillo, R.A., Sayward, F.G.: Mutation Analysis. Yale University, Department of Computer Science, New Haven (1979)"},{"key":"240_CR19","unstructured":"Buxton, J.N., Randell, B.: Report of a conference sponsored by the NATO science committee. In: NATO Software Engineering Conference, vol. 1969 (1969)"},{"key":"240_CR20","doi-asserted-by":"crossref","unstructured":"Chen, Y., Groce, A., Zhang, C., Wong, W.K., Fern, X., Eide, E., Regehr, J.: Taming compiler fuzzers. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 197\u2013208 (2013)","DOI":"10.1145\/2499370.2462173"},{"key":"240_CR21","doi-asserted-by":"crossref","unstructured":"Chockler, H., Gurfinkel, A., Strichman, O.: Beyond vacuity: Towards the strongest passing formula. In: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, pp. 24:1\u201324:8 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.28"},{"key":"240_CR22","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","volume-title":"Computer Aided Verification","author":"Hana Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Computer Aided Verification, pp. 66\u201378 (2001)"},{"issue":"5","key":"240_CR23","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1109\/TCAD.2011.2180382","volume":"31","author":"H Chockler","year":"2012","unstructured":"Chockler, H., Kroening, D., Purandare, M.: Computing mutation coverage in interpolation-based model checking. IEEE Trans. CAD Integr. Circuits Syst. 31(5), 765\u2013778 (2012)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"240_CR24","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Design Automation Conference, pp. 427\u2013432 (1995)","DOI":"10.21236\/ADA288583"},{"key":"240_CR25","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"240_CR26","first-page":"120","volume-title":"Lecture Notes in Computer Science","author":"Pascal Cuoq","year":"2012","unstructured":"Cuoq, P., Monate, B., Pacalet, A., Prevosto, V., Regehr, J., Yakobowski, B., Yang, X.: Testing static analyzers with randomly generated programs. In: NASA Formal Methods Symposium, pp. 120\u2013125 (2012)"},{"key":"240_CR27","doi-asserted-by":"crossref","unstructured":"Daran, M., Th\u00e9venod-Fosse, P.: Software error analysis: A real case study involving real faults and mutations. In: ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 158\u2013171. ACM (1996)","DOI":"10.1145\/226295.226313"},{"key":"240_CR28","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"11","key":"240_CR29","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 (1978)","journal-title":"Computer"},{"key":"240_CR30","unstructured":"Desnoyers, M.: [RFC git tree] userspace RCU (urcu) for Linux (2009). http:\/\/urcu.so"},{"key":"240_CR31","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1109\/TPDS.2011.159","volume":"23","author":"M Desnoyers","year":"2012","unstructured":"Desnoyers, M., McKenney, P.E., Stern, A., Dagenais, M.R., Walpole, J.: User-level implementations of read-copy update. IEEE Trans. Parallel Distrib. Syst. 23, 375\u2013382 (2012). https:\/\/doi.org\/10.1109\/TPDS.2011.159","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"240_CR32","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ (1976)"},{"key":"240_CR33","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"Niklas E\u00e9n","year":"2004","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Symposium on the Theory and Applications of Satisfiability Testing (SAT), pp. 502\u2013518 (2003)"},{"key":"240_CR34","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., Gacek, A., Whalen, M.W., Heimdahl, M.P.E., Wagner, L.G.: Proof-based coverage metrics for formal verification. In: IEEE\/ACM International Conference on Automated Software Engineering, pp. 194\u2013199 (2017a)","DOI":"10.1109\/ASE.2017.8115632"},{"key":"240_CR35","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., Gacek, A., Whalen, M.W.: Efficient generation of inductive validity cores for safety properties. In: ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 314\u2013325 (2016)","DOI":"10.1145\/2950290.2950346"},{"key":"240_CR36","doi-asserted-by":"crossref","unstructured":"Ghassabani, E., Whalen, M.W., Gacek, A.: Efficient generation of all minimal inductive validity cores. In: FMCAD, pp. 31\u201338 (2017b)","DOI":"10.23919\/FMCAD.2017.8102238"},{"key":"240_CR37","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Groce, A., Zhang, C., Sharma, R., Alipour, A., Marinov, D.: Comparing non-adequate test suites using coverage criteria. In: International Symposium on Software Testing and Analysis, pp. 302\u2013313 (2013)","DOI":"10.1145\/2483760.2483769"},{"key":"240_CR38","unstructured":"Gligoric, M., Groce, A., Zhang, C., Sharma, R., Alipour, A., Marinov, D.: Guidelines for coverage-based comparisons of non-adequate test suites. ACM Trans. Softw. Eng. Methodol.(accepted for publication)"},{"key":"240_CR39","doi-asserted-by":"crossref","unstructured":"Gopinath, R., Jensen, C., Groce, A.: Code coverage for suite evaluation by developers. In: International Conference on Software Engineering, pp. 72\u201382 (2014)","DOI":"10.1145\/2568225.2568278"},{"key":"240_CR40","doi-asserted-by":"publisher","unstructured":"Groce, A., Ahmed, I., Jensen, C., McKenney, P.E.: How verified is my code? falsification-driven verification. In: 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9\u201313, 2015, pp. 737\u2013748 (2015). https:\/\/doi.org\/10.1109\/ASE.2015.40","DOI":"10.1109\/ASE.2015.40"},{"key":"240_CR41","doi-asserted-by":"crossref","unstructured":"Groce, A., Alipour, M.A., Gopinath, R.: Coverage and its discontents. In: Onward! Essays, pp. 255\u2013268 (2014)","DOI":"10.1145\/2661136.2661157"},{"key":"240_CR42","doi-asserted-by":"crossref","unstructured":"Groce, A., Erwig, M.: Finding common ground: choose, assert, and assume. In: Workshop on Dynamic Analysis, pp. 12\u201317 (2012)","DOI":"10.1145\/2338966.2336800"},{"key":"240_CR43","doi-asserted-by":"crossref","unstructured":"Groce, A., Holmes, J., Marinov, D., Shi, A., Zhang, L.: An extensible, regular-expression-based tool for multi-language mutant generation. In: International Conference on Software Engineering (2018)","DOI":"10.1145\/3183440.3183485"},{"key":"240_CR44","doi-asserted-by":"crossref","unstructured":"Groce, A., Holzmann, G., Joshi, R., Xu, R.G.: Putting flight software through the paces with testing, model checking, and constraint-solving. In: Workshop on Constraints in Formal Verification, pp. 1\u201315 (2008)","DOI":"10.1007\/s10515-008-0033-9"},{"key":"240_CR45","doi-asserted-by":"crossref","unstructured":"Groce, A., Holzmann, G., Joshi, R.: Randomized differential testing as a prelude to formal verification. In: International Conference on Software Engineering, pp. 621\u2013631 (2007)","DOI":"10.1109\/ICSE.2007.68"},{"key":"240_CR46","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/11691372_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Alex Groce","year":"2006","unstructured":"Groce, A., Joshi, R.: Exploiting traces in program analysis. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 379\u2013393 (2006)"},{"key":"240_CR47","doi-asserted-by":"crossref","unstructured":"Groce, A., Joshi, R.: Random testing and model checking: Building a common framework for nondeterministic exploration. In: Workshop on Dynamic Analysis, pp. 22\u201328 (2008)","DOI":"10.1145\/1401827.1401833"},{"key":"240_CR48","unstructured":"Groce, A., Pinto, J., Azimi, P., Mittal, P., Holmes, J., Kellar, K.: TSTL: the template scripting testing language. https:\/\/github.com\/agroce\/tstl (2015b)"},{"key":"240_CR49","doi-asserted-by":"crossref","unstructured":"Groce, A., Pinto, J., Azimi, P., Mittal, P.: TSTL: a language and tool for testing (demo). In: ACM International Symposium on Software Testing and Analysis, pp. 414\u2013417 (2015a)","DOI":"10.1145\/2771783.2784769"},{"key":"240_CR50","first-page":"204","volume-title":"Lecture Notes in Computer Science","author":"Alex Groce","year":"2015","unstructured":"Groce, A., Pinto, J.: A little language for testing. In: NASA Formal Methods Symposium, pp. 204\u2013218 (2015)"},{"key":"240_CR51","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-24730-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Alex Groce","year":"2004","unstructured":"Groce, A.: Error explanation with distance metrics. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 108\u2013122 (2004)"},{"key":"240_CR52","doi-asserted-by":"crossref","unstructured":"Groce, A.: Quickly testing the tester via path coverage. In: Workshop on Dynamic Analysis (2009)","DOI":"10.1145\/2134243.2134249"},{"issue":"2","key":"240_CR53","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.entcs.2004.12.023","volume":"119","author":"A Groce","year":"2005","unstructured":"Groce, A., Kroening, D.: Making the most of BMC counter examples. Electron. Notes Theor. Comput. Sci. 119(2), 67\u201381 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"240_CR54","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1147\/sj.472.0221","volume":"47","author":"D Guniguntala","year":"2008","unstructured":"Guniguntala, D., McKenney, P.E., Triplett, J., Walpole, J.: The read-copy-update mechanism for supporting real-time applications on shared-memory multiprocessor systems with Linux. IBM Syst. J. 47(2), 221\u2013236 (2008)","journal-title":"IBM Syst. J."},{"issue":"1","key":"240_CR55","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10009-016-0445-y","volume":"20","author":"Josie Holmes","year":"2016","unstructured":"Holmes, J., Groce, A., Pinto, J., Mittal, P., Azimi, P., Kellar, K., O\u2019Brien, J.: TSTL: the template scripting testing language. Int. J. Softw. Tools Technol. Transf. (2016). https:\/\/doi.org\/10.1007\/s10009-016-0445-y . (Online first)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"6","key":"240_CR56","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1002\/spe.4380100608","volume":"10","author":"RN Horspool","year":"1980","unstructured":"Horspool, R.N.: Practical fast searching in strings. Softw. Pract. Exp. 10(6), 501\u2013506 (1980)","journal-title":"Softw. Pract. Exp."},{"key":"240_CR57","doi-asserted-by":"crossref","unstructured":"Hoskote, Y., Kam, T., Ho, P.H., Zhao, X.: Coverage estimation for symbolic model checking. In: ACM\/IEEE Design Automation Conference, pp. 300\u2013305 (1999)","DOI":"10.1145\/309847.309936"},{"key":"240_CR58","doi-asserted-by":"publisher","DOI":"10.1093\/oseo\/instance.00032980","volume-title":"An Enquiry Concerning Human Understanding","author":"D Hume","year":"1748","unstructured":"Hume, D.: An Enquiry Concerning Human Understanding. Routledge, London (1748)"},{"key":"240_CR59","doi-asserted-by":"crossref","unstructured":"Just, R., Jalali, D., Inozemtseva, L., Ernst, M.D., Holmes, R., Fraser, G.: Are mutants a valid substitute for real faults in software testing? In: ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 654\u2013665 (2014)","DOI":"10.1145\/2635868.2635929"},{"key":"240_CR60","volume-title":"Lessons Learned in Software Testing: A Context-Driven Approach","author":"C Kaner","year":"2001","unstructured":"Kaner, C., Bach, J., Pettichord, B.: Lessons Learned in Software Testing: A Context-Driven Approach. Wiley, Hoboken (2001)"},{"key":"240_CR61","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E.M., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"240_CR62","first-page":"298","volume-title":"Lecture Notes in Computer Science","author":"Daniel Kroening","year":"2002","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Verification, Model Checking, and Abstract Interpretation, pp. 298\u2013309 (2003)"},{"key":"240_CR63","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Li, W., Seshia, S.: A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: Formal Methods in Computer-Aided Design, pp. 1\u20139 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.29"},{"issue":"4","key":"240_CR64","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/0039-3681(74)90007-7","volume":"4","author":"I Lakatos","year":"1974","unstructured":"Lakatos, I.: The role of crucial experiments in science. Stud. His. Philos. Sci. Part A 4(4), 309\u2013325 (1974)","journal-title":"Stud. His. Philos. Sci. Part A"},{"key":"240_CR65","unstructured":"Lawlor, R.: quicksort.c. http:\/\/www.comp.dit.ie\/rlawlor\/Alg_DS\/sorting\/quickSort.c . Referenced April 20 (2015)"},{"key":"240_CR66","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-540-30476-0_29","volume-title":"Automated Technology for Verification and Analysis","author":"Te-Chang Lee","year":"2004","unstructured":"Lee, T.C., Hsiung, P.A.: Mutation coverage estimation for model checking. In: Automated Technology for Verification and Analysis, pp. 354\u2013368 (2004)"},{"key":"240_CR67","unstructured":"Lipton, R.J.: Fault diagnosis of computer programs. Carnegie Mellon Univ, Technical Report (1971)"},{"key":"240_CR68","unstructured":"Liu, X.: muupi mutation tool. https:\/\/github.com\/apepkuss\/muupi (2016)"},{"key":"240_CR69","volume-title":"Foundations of Software Testing","author":"AP Mathur","year":"2012","unstructured":"Mathur, A.P.: Foundations of Software Testing. Addison-Wesley, Boston (2012)"},{"issue":"1","key":"240_CR70","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1002\/stvr.4370040104","volume":"4","author":"AP Mathur","year":"1994","unstructured":"Mathur, A.P., Wong, W.E.: An empirical comparison of data flow and mutation-based test adequacy criteria. J. Softw. Test. Verif. Reliab. 4(1), 9\u201331 (1994)","journal-title":"J. Softw. Test. Verif. Reliab."},{"issue":"1","key":"240_CR71","first-page":"100","volume":"10","author":"W McKeeman","year":"1998","unstructured":"McKeeman, W.: Differential testing for software. Dig. Tech. J. Dig. Equip. Corp. 10(1), 100\u2013107 (1998)","journal-title":"Dig. Tech. J. Dig. Equip. Corp."},{"key":"240_CR72","unstructured":"McKenney, P.E., Eggemann, D., Randhawa, R.: Improving energy efficiency on asymmetric multiprocessing systems (2013). https:\/\/www.usenix.org\/system\/files\/hotpar13-poster8-mckenney.pdf"},{"key":"240_CR73","unstructured":"McKenney, P.E., Slingwine, J.D.: Read-copy update: Using execution history to solve concurrency problems. In: Parallel and Distributed Computing and Systems, pp. 509\u2013518. Las Vegas, NV (1998)"},{"key":"240_CR74","unstructured":"McKenney, P.E.: RCU Linux usage (2006). Available: http:\/\/www.rdrop.com\/users\/paulmck\/RCU\/linuxusage.html (Viewed January 14, 2007)"},{"key":"240_CR75","unstructured":"McKenney, P.E.: RCU torture test operation. https:\/\/www.kernel.org\/doc\/Documentation\/RCU\/torture.txt"},{"key":"240_CR76","unstructured":"McKenney, P.E.: Re: [PATCH fyi] RCU: the bloatwatch edition (2009). Available: http:\/\/lkml.org\/lkml\/2009\/1\/14\/449 (Viewed January 15, 2009)"},{"key":"240_CR77","unstructured":"McKenney, P.E.: Verification challenge 4: Tiny RCU. http:\/\/paulmck.livejournal.com\/39343.html (2015a)"},{"key":"240_CR78","unstructured":"McKenney, P.E.: Verification challenge 5: Uses of RCU. http:\/\/paulmck.livejournal.com\/39793.html (2015b)"},{"issue":"7","key":"240_CR79","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/2483852.2483867","volume":"56","author":"PE McKenney","year":"2013","unstructured":"McKenney, P.E.: Structured deferral: synchronization via procrastination. Commun. ACM 56(7), 40\u201349 (2013). https:\/\/doi.org\/10.1145\/2483852.2483867","journal-title":"Commun. ACM"},{"key":"240_CR80","first-page":"279","volume-title":"Lecture Notes in Computer Science","author":"Anitha Murugesan","year":"2015","unstructured":"Murugesan, A., Whalen, M.W., Rungta, N., Tkachuk, O., Person, S., Heimdahl, M.P.E., You, D.: Are we there yet? determining the adequacy of formalized requirements and test suites. In: NASA Formal Methods Symposium, pp. 279\u2013294 (2015)"},{"key":"240_CR81","unstructured":"Offutt, A.J., Voas, J.M.: Subsumption of condition coverage techniques by mutation testing. In: Technical Report ISSE-TR-96-01, Information and Software Systems Engineering, George Mason University (1996)"},{"key":"240_CR82","doi-asserted-by":"crossref","unstructured":"Papadakis, M., Jia, Y., Harman, M., Traon, Y.L.: Trivial compiler equivalence: A large scale empirical study of a simple fast and effective equivalent mutant detection technique. In: International Conference on Software Engineering (2015)","DOI":"10.1109\/ICSE.2015.103"},{"key":"240_CR83","volume-title":"The Logic of Scientific Discovery","author":"K Popper","year":"1959","unstructured":"Popper, K.: The Logic of Scientific Discovery. Routledge, Hutchinson (1959)"},{"key":"240_CR84","volume-title":"Conjectures and Refutations: The Growth of Scientific Knowledge","author":"K Popper","year":"1963","unstructured":"Popper, K.: Conjectures and Refutations: The Growth of Scientific Knowledge. Routledge, London (1963)"},{"key":"240_CR85","doi-asserted-by":"crossref","unstructured":"Schuler, D., Zeller, A.: Assessing oracle quality with checked coverage. In: International Conference on Software Testing, Verification and Validation, pp. 90\u201399 (2011)","DOI":"10.1109\/ICST.2011.32"},{"issue":"7","key":"240_CR86","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1002\/stvr.1497","volume":"23","author":"D Schuler","year":"2013","unstructured":"Schuler, D., Zeller, A.: Checked coverage: an indicator for oracle quality. Softw. Test. Verif. Reliab. 23(7), 531\u2013551 (2013)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"240_CR87","unstructured":"scvalex: Finding all paths of minimum length to a node using dijkstras algorithm. https:\/\/compprog.wordpress.com\/2008\/01\/17\/finding-all-paths-of-minimum-length-to-a-node-using-dijkstras-algorithm\/ (2008)"},{"key":"240_CR88","unstructured":"Stout, R.: If Death Ever Slept. Viking (1957)"},{"key":"240_CR89","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-69149-5_54","volume-title":"Verified Software: Theories, Tools, Experiments","author":"Ofer Strichman","year":"2008","unstructured":"Strichman, O., Godlin, B.: Regression verification-a practical way to verify programs. Verified Software: Theories, Tools, Experiments pp. 496\u2013501 (2008)"},{"key":"240_CR90","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Dreyer, D., Vafeiadis, V.: Verifying read-copy-update in a logic for weak memory. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (2015). (To appear)","DOI":"10.1145\/2737924.2737992"},{"key":"240_CR91","first-page":"121","volume":"3","author":"F Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. J. Program. Lang. 3, 121\u2013189 (1995)","journal-title":"J. Program. Lang."},{"key":"240_CR92","unstructured":"visar: [SOLVED] doubly linked list insertion sort in C. http:\/\/www.linuxquestions.org\/questions\/programming-9\/doubly-linked-list-insertion-sort-in-c-4175415860\/ (2012)"},{"issue":"2","key":"240_CR93","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"240_CR94","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 283\u2013294 (2011)","DOI":"10.1145\/1993316.1993532"},{"key":"240_CR95","doi-asserted-by":"crossref","unstructured":"Zhang, X., Gupta, R., Zhang, Y.: Precise dynamic slicing algorithms. In: International Conference on Software Engineering, pp. 319\u2013329 (2003)","DOI":"10.1109\/ICSE.2003.1201211"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-018-0240-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-018-0240-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-018-0240-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T18:25:28Z","timestamp":1751739928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-018-0240-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,11]]},"references-count":95,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["240"],"URL":"https:\/\/doi.org\/10.1007\/s10515-018-0240-y","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,11]]},"assertion":[{"value":"11 December 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 July 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}