{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:38:26Z","timestamp":1780115906930,"version":"3.54.0"},"reference-count":115,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T00:00:00Z","timestamp":1395100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10472-014-9408-8","type":"journal-article","created":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T05:57:04Z","timestamp":1395122224000},"page":"315-349","source":"Crossref","is-referenced-by-count":25,"title":["Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning"],"prefix":"10.1007","volume":"70","author":[{"given":"Alex","family":"Groce","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerard","family":"Holzmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rajeev","family":"Joshi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ru-Gang","family":"Xu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2014,3,18]]},"reference":[{"key":"9408_CR1","unstructured":"About Static Driver Verifier: http:\/\/www.microsoft.com\/whdc\/DevTools\/tools\/SDV.mspx"},{"key":"9408_CR2","unstructured":"ACL2 Version 6.3: http:\/\/www.cs.utexas.edu\/moore\/acl2"},{"key":"9408_CR3","unstructured":"AdaCore: SPARK Pro. http:\/\/www.adacore.com\/sparkpro\/"},{"key":"9408_CR4","unstructured":"CodeSonar: GrammaTech static analysis. http:\/\/www.grammatech.com\/products\/codesonar"},{"key":"9408_CR5","unstructured":"Hyper-V - Microsoft: http:\/\/www.microsoft.com\/servers\/hyper-v-server\/default.mspx"},{"key":"9408_CR6","unstructured":"JPL Laboratory for Reliable Software (LaRS): http:\/\/lars-lab.jpl.nasa.gov"},{"key":"9408_CR7","unstructured":"Mars Science Laboratory: http:\/\/mars.jpl.nasa.gov\/msl"},{"key":"9408_CR8","unstructured":"Open Group Base Specifications Issue 6: http:\/\/www.opengroup.org\/onlinepubs\/009695399\/"},{"key":"9408_CR9","unstructured":"Software development testing and static analysis tools: Coverity. http:\/\/www.coverity.com"},{"key":"9408_CR10","unstructured":"Source code analysis tools for software security & reliability: Klockwork. http:\/\/klocwork.com"},{"key":"9408_CR11","unstructured":"VCC: A C verifier - Microsoft Research: http:\/\/research.microsoft.com\/en-us\/projects\/vcc\/"},{"key":"9408_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809163","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2008","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008)"},{"key":"9408_CR13","doi-asserted-by":"crossref","unstructured":"Andrews, J., Li, F., Menzies, T.: Nighthawk: a two-level genetic-random unit test data generator. Autom. Softw. Eng. 144\u2013153 (2007)","DOI":"10.1145\/1321631.1321654"},{"key":"9408_CR14","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"},{"key":"9408_CR15","doi-asserted-by":"crossref","unstructured":"Andrews, J.H., Haldar, S., Lei, Y., Li, C.H.F.: Tool support for randomized unit testing. In: Proceedings of the First International Workshop on Randomized Testing, pp. 36\u201345. Portland (2006)","DOI":"10.1145\/1145735.1145741"},{"issue":"2","key":"9408_CR16","first-page":"87106","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Info. Comput. 75(2), 87106 (1987)","journal-title":"Info. Comput."},{"key":"9408_CR17","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software, pp. 103\u2013122 (2001)","DOI":"10.1007\/3-540-45139-0_7"},{"issue":"11","key":"9408_CR18","doi-asserted-by":"crossref","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.: Formal analysis of log files. J. Aerosp. Comput. Info. Commun. 7(11), 365\u2013390 (2010)","journal-title":"J. Aerosp. Comput. Info. Commun."},{"key":"9408_CR19","doi-asserted-by":"crossref","unstructured":"Barringer, H., Havelund, K., Rydeheard, D., Groce, A.: Rule systems for runtime verification: a short tutorial. In: Proceedings of the 9th International Workshop on Runtime Verification (RV\u201909), LNCS, vol. 5779, pp. 1\u201324. Springer (2009)","DOI":"10.1007\/978-3-642-04694-0_1"},{"key":"9408_CR20","doi-asserted-by":"crossref","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. In: Proceedings of the 7th International Workshop on Runtime Verification (RV\u201907), LNCS, vol. 4839, pp. 111\u2013125. Springer, Vancouver (2007)","DOI":"10.1007\/978-3-540-77395-5_10"},{"issue":"3","key":"9408_CR21","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. 20(3), 675\u2013706 (2010)","journal-title":"J. Log. Comput."},{"key":"9408_CR22","volume-title":"Test Driven Development: By Example","author":"K Beck","year":"2002","unstructured":"Beck, K.: Test Driven Development: By Example. Addison Wesley, Reading (2002)"},{"key":"9408_CR23","unstructured":"Beizer, B.: Software Testing Techniques. International Thomson Computer Press, Boston (1990)"},{"key":"9408_CR24","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: International Conference on Software Engineering, pp. 326\u2013335 (2004)","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"9408_CR25","unstructured":"Biere, A.: The Evolution from Limmat to Nanosat. Technical Report 444, Dept. of Computer Science, ETH Z\u016drich (2004)"},{"key":"9408_CR26","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"9408_CR27","doi-asserted-by":"crossref","first-page":"592","DOI":"10.1109\/TC.1972.5009015","volume":"21","author":"AW Biermann","year":"1972","unstructured":"Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behaviour. IEEE Trans. Comput. 21, 592\u2013597 (1972)","journal-title":"IEEE Trans. Comput."},{"key":"9408_CR28","doi-asserted-by":"crossref","unstructured":"Boonstoppel, P., Cadar, C., Engler, D.: Rwset: attacking path explosion in constraint-based test generation. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 351\u2013366 (2008)","DOI":"10.1007\/978-3-540-78800-3_27"},{"key":"9408_CR29","unstructured":"Brooks, F.: The Mythical Man-Month: Essays on Software Engineering, 20th Anniversary Edition. Addison-Wesley Professional (1995)"},{"key":"9408_CR30","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Operating System Design and Implementation, pp. 209\u2013224 (2008)"},{"key":"9408_CR31","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., Engler, D.: EXE: automatically generating inputs of death. In: Conference on Computer and Communications Security, pp. 322\u2013335 (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"9408_CR32","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: International Conference on Software Engineering, pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"9408_CR33","doi-asserted-by":"crossref","unstructured":"Chen, F., Ro\u015fu, G.: MOP: an efficient and generic runtime verification framework. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA\u201907) (2007)","DOI":"10.1145\/1297027.1297069"},{"key":"9408_CR34","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\/2491956.2462173"},{"key":"9408_CR35","doi-asserted-by":"crossref","unstructured":"Ciupa, I., Leitner, A., Oriol, M., Meyer, B.: Experimental assessment of random testing for object-oriented software. In: Rosenblum, D.S., Elbaum, S.G. (eds.) International Symposium on Software Testing and Analysis, pp 84\u201394. ACM (2007)","DOI":"10.1145\/1273463.1273476"},{"key":"9408_CR36","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of haskell programs. In: ICFP, pp. 268\u2013279 (2000)","DOI":"10.1145\/357766.351266"},{"key":"9408_CR37","volume-title":"Model Checking","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"9408_CR38","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.: The design and synthesis of synchronization skeletons using temporal logic. In: Workshop on Logics of Programs, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"issue":"3","key":"9408_CR39","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/1127878.1127900","volume":"31","author":"LA Clarke","year":"2006","unstructured":"Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Softw. Eng. Notes 31(3), 25\u201337 (2006)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"9408_CR40","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C.S., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: International Conference on Software Engineering, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"issue":"11","key":"9408_CR41","doi-asserted-by":"crossref","first-page":"1025","DOI":"10.1002\/spe.602","volume":"34","author":"C Csallner","year":"2004","unstructured":"Csallner, C., Smaragdakis, Y.: JCrasher: an automatic robustness tester for Java. Softw. Pract. Exp. 34(11), 1025\u20131050 (2004)","journal-title":"Softw. Pract. Exp."},{"key":"9408_CR42","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bjorner, N.: Z3: an efficient SMT solver. In: Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9408_CR43","doi-asserted-by":"crossref","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)","DOI":"10.1109\/C-M.1978.218136"},{"issue":"2","key":"9408_CR44","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1145\/192218.192221","volume":"3","author":"R-K Doong","year":"1994","unstructured":"Doong, R.-K., Frankl, P.G.: The ASTOOT approach to testing object-oriented programs. ACM Trans. Softw. Eng. Methodol. 3(2), 101\u2013130 (1994)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"4","key":"9408_CR45","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1109\/TSE.1984.5010257","volume":"10","author":"JW Duran","year":"1984","unstructured":"Duran, J.W., Ntafos, S.C.: Evaluation of random testing. IEEE Trans. Softw. Eng. 10(4), 438\u2013444 (1984)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9408_CR46","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel randomized state-space search. In: International Conference on Software Engineering, pp. 3\u201312 (2007)","DOI":"10.21236\/ADA459092"},{"key":"9408_CR47","doi-asserted-by":"crossref","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Symposium on the Theory and Applications of Satisfiability Testing (SAT), pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9408_CR48","unstructured":"Erickson, J., Joshi, R.: Proving Correctness of a Flash Filesystem in ACL2. Unpublished manuscript in preparation (2006)"},{"key":"9408_CR49","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":"9408_CR50","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Verisoft: a tool for the automatic analysis of concurrent software. In: Computer-Aided Verification, pp. 172\u2013186 (1997)","DOI":"10.1007\/3-540-63166-6_52"},{"key":"9408_CR51","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Principles of Programming Languages, pp. 47\u201354 (2007)","DOI":"10.1145\/1190215.1190226"},{"key":"9408_CR52","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Programming Language Design and Implementation, pp. 213\u2013223 (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"9408_CR53","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"},{"key":"9408_CR54","doi-asserted-by":"crossref","unstructured":"Groce, A., Fern, A., Pinto, J., Bauer, T., Alipour, A., Erwig, M., Lopez, C.: Lightweight automated testing with adaptation-based programming. In: IEEE International Symposium on Software Reliability Engineering, pp. 161\u2013170 (2012)","DOI":"10.1109\/ISSRE.2012.1"},{"key":"9408_CR55","doi-asserted-by":"crossref","unstructured":"Groce, A., Havelund, K., Smith, M.H.: From scripts to specifications: the evolution of a flight software testing effort. In: 32nd International Conference on Software Engineering (ICSE\u201910), pp. 129\u2013138. ACM SIG, Cape Town (2010)","DOI":"10.1145\/1810295.1810314"},{"key":"9408_CR56","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":"9408_CR57","unstructured":"Groce, A., Holzmann, G., Joshi, R., Xu, R.-G.: Putting flight software through the paces with testing, model checking, and constraint-solving. In: International Workshop on Constraints in Formal Verification, pp. 1\u201315 (2008)"},{"key":"9408_CR58","doi-asserted-by":"crossref","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)","DOI":"10.1007\/11691372_25"},{"key":"9408_CR59","doi-asserted-by":"crossref","unstructured":"Groce, A., Joshi, R.: Extending model checking with dynamic analysis. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 142\u2013156 (2008)","DOI":"10.1007\/978-3-540-78163-9_15"},{"key":"9408_CR60","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":"9408_CR61","doi-asserted-by":"crossref","unstructured":"Groce, A., Zhang, C., Alipour, A., Eide, E., Chen, Y., Regehr, J.: Help, help, I\u2019m being suppressed! the significance of suppressors in software testing. In: IEEE International Symposium on Software Reliability Engineering, pp. 390\u2013399 (2013)","DOI":"10.1109\/ISSRE.2013.6698892"},{"key":"9408_CR62","doi-asserted-by":"crossref","unstructured":"Groce, A., Zhang, C., Eide, E., Chen, Y., Regehr, J.: Swarm testing. In: International Symposium on Software Testing and Analysis, pp. 78\u201388 (2012)","DOI":"10.1145\/2338965.2336763"},{"key":"9408_CR63","unstructured":"Hamlet, R.: Testing programs with the aid of a compiler. IEEE Trans. Softw. Eng. 3(4), 279\u2013290 (1977)"},{"issue":"12","key":"9408_CR64","doi-asserted-by":"crossref","first-page":"1402","DOI":"10.1109\/32.62448","volume":"16","author":"R Hamlet","year":"1990","unstructured":"Hamlet, R., Taylor, R.: Partition testing does not inspire confidence. IEEE Trans. Softw. Eng. 16(12), 1402\u20131411 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9408_CR65","unstructured":"Hamlet, R.: Random testing. In: Encyclopedia of Software Engineering, pp. 970\u2013978. Wiley (1994)"},{"key":"9408_CR66","doi-asserted-by":"crossref","unstructured":"Hamlet, R.: When only random testing will do. In: International Workshop on Random Testing, pp. 1\u20139 (2006)","DOI":"10.1145\/1145735.1145737"},{"key":"9408_CR67","doi-asserted-by":"crossref","unstructured":"Havelund, K.: Runtime verification of C programs. In: Proceedings of the 1st TestCom\/FATES Conference, LNCS, vol. 5047. Springer, Tokyo (2008)","DOI":"10.1007\/978-3-540-68524-1_3"},{"issue":"2","key":"9408_CR68","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: Efficient monitoring of safety properties. Softw. Tools Technol. Tran. 6(2), 158\u2013173 (2004)","journal-title":"Softw. Tools Technol. Tran."},{"key":"9408_CR69","doi-asserted-by":"crossref","unstructured":"Heimdahl, M.P.E., Rayadurgam, S., Visser, W., George, D., Gao, J.: Auto-generating test sequences using model checkers: a case study. In: International Workshop on Formal Approaches to Testing of Software (FATES) (2003)","DOI":"10.1007\/978-3-540-24617-6_4"},{"key":"9408_CR70","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"issue":"1","key":"9408_CR71","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: a grand challenge for computing research. J. ACM 50(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"9408_CR72","unstructured":"Holzmann, G.: Static source code checking for user-defined properties. In: Conference on Integrated Design and Process Technology (2002)"},{"key":"9408_CR73","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)"},{"issue":"6","key":"9408_CR74","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1109\/MC.2006.212","volume":"39","author":"G Holzmann","year":"2006","unstructured":"Holzmann, G.: The power of ten: rules for developing safety critical code. IEEE Comput. 39(6), 95\u201397 (2006)","journal-title":"IEEE Comput."},{"key":"9408_CR75","doi-asserted-by":"crossref","unstructured":"Holzmann, G., Joshi, R.: Model-driven software verification. In: SPIN Workshop on Model Checking of Software, pp. 76\u201391 (2004)","DOI":"10.1007\/978-3-540-24732-6_6"},{"key":"9408_CR76","doi-asserted-by":"crossref","unstructured":"Holzmann, G., Joshi, R., Groce, A.: Swarm verification. In: Automated Software Engineering, pp. 1\u20136 (2008)","DOI":"10.1109\/ASE.2008.9"},{"key":"9408_CR77","doi-asserted-by":"crossref","unstructured":"Holzmann, G., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: SPIN Workshop on Model Checking of Software, pp. 134\u2013143 (2008)","DOI":"10.1007\/978-3-540-85114-1_11"},{"issue":"6","key":"9408_CR78","doi-asserted-by":"crossref","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"GJ Holzmann","year":"2011","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845\u2013857 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9408_CR79","unstructured":"Joshi, R., Holzmann, G.: A mini-challenge: build a verifiable filesystem. In: The Conference on Verified Software: Theories, Tools, Experiments (2005)"},{"key":"9408_CR80","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Norwell (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"9408_CR81","doi-asserted-by":"crossref","unstructured":"Kim, M., Choi, Y., Kim, Y., Kim, H.: Formal verification of a flash memory device driver \u2014 an experience report. In: SPIN Workshop on Model Checking of Software, pp. 144\u2013159 (2008)","DOI":"10.1007\/978-3-540-85114-1_12"},{"key":"9408_CR82","doi-asserted-by":"crossref","unstructured":"Kim, M., Choi, Y., Kim, Y., Kim, H.: Pre-testing flash device driver through model checking techniques. In: International Conference on Software Testing, Verification, and Validation, pp. 475\u2013484 (2008)","DOI":"10.1109\/ICST.2008.55"},{"key":"9408_CR83","unstructured":"Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance tool for Java. In: Proceedings of the 1st International Workshop on Runtime Verification (RV\u201901) of ENTCS, vol. 55, issue 2. Elsevier (2001)"},{"key":"9408_CR84","doi-asserted-by":"crossref","unstructured":"Kim, M., Kim, Y., Kim, H.: Unit testing of flash memory device driver through a SAT-based model checker. In: Automated Software Engineering, pp. 198\u2013207 (2008)","DOI":"10.1109\/ASE.2008.30"},{"issue":"7","key":"9408_CR85","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"9408_CR86","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: sel4: formal verification of an OS kernel. In: ACM Symposium on Operating Systems Principles (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"9408_CR87","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":"9408_CR88","unstructured":"Lei, Y., Andrews, J.H.: Minimization of randomized unit test cases. In: International Symposium on Software Reliability Engineering, pp. 267\u2013276 (2005)"},{"key":"9408_CR89","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: International Conference on Software Engineering, pp. 416\u2013426 (2007)","DOI":"10.1109\/ICSE.2007.41"},{"issue":"1","key":"9408_CR90","first-page":"100","volume":"10","author":"W McKeeman","year":"1998","unstructured":"McKeeman, W.: Differential testing for software. Digit. Tech. J. Digit. Equip. Corp. 10(1), 100\u2013107 (1998)","journal-title":"Digit. Tech. J. Digit. Equip. Corp."},{"key":"9408_CR91","doi-asserted-by":"crossref","unstructured":"Mercer, E., Jones, M.: Model checking machine code with the GNU debugger. In: SPIN Workshop on Model Checking Software (2005)","DOI":"10.1007\/11537328_20"},{"key":"9408_CR92","doi-asserted-by":"crossref","unstructured":"Miller, B.P., Fredriksen, L., So, B.: An empirical study of the reliability of UNIX utilities. Commun. ACM 105(33(12)), 32\u201344 (1990)","DOI":"10.1145\/96267.96279"},{"key":"9408_CR93","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9408_CR94","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: a pragmatic approach to model checking real code. In: Symposium on Operating System Design and Implementation (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"9408_CR95","doi-asserted-by":"crossref","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: International Conference on Compiler Construction, pp. 213\u2013228 (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"9408_CR96","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9408_CR97","unstructured":"Offutt, J., Abdurazik, A.: Mutation 2000: Mutation Testing in the Twentieth and the Twenty First Centuries (2000)"},{"key":"9408_CR98","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: International Conference on Software Engineering, pp. 75\u201384 (2007)","DOI":"10.1109\/ICSE.2007.37"},{"key":"9408_CR99","unstructured":"Pettichord, B.: Design for testability. In: Pacific Northwest Software Quality Conference (2002)"},{"key":"9408_CR100","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 93\u2013107 (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"9408_CR101","doi-asserted-by":"crossref","unstructured":"Reeves, G., Neilson, T.: The mars rover spirit FLASH anomaly. In: IEEE Aerospace Conference (2005)","DOI":"10.1109\/AERO.2005.1559723"},{"key":"9408_CR102","doi-asserted-by":"crossref","unstructured":"Dwyer, R.M., Hatcliff, J.: Bogor: an extensible and highly-modular model checking framework. In: European Software Engineering Conference\/Symposium on the Foundations of Software Engineering, pp. 267\u2013276 (2003)","DOI":"10.1145\/949952.940107"},{"key":"9408_CR103","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Foundations of Software Engineering, pp. 262\u2013272 (2005)","DOI":"10.21236\/ADA482657"},{"key":"9408_CR104","doi-asserted-by":"crossref","unstructured":"Smith, M., Havelund, K.: Requirements capture with RCAT. In: 16th IEEE International Requirements Engineering Conference (RE\u201908). IEEE Computer Society, Barcelona (2008)","DOI":"10.1109\/RE.2008.50"},{"key":"9408_CR105","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Principles of Programming Languages, pp. 97\u2013108 (2007)","DOI":"10.1145\/1190215.1190234"},{"key":"9408_CR106","unstructured":"Various: A Collection of NAND Flash Application Notes, Whitepapers and Articles. Available at http:\/\/www.data-io.com\/NAND\/NANDApplicationNotes.asp"},{"key":"9408_CR107","unstructured":"Runtime Verification: http:\/\/www.runtime-verification.org"},{"issue":"2","key":"9408_CR108","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.J., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"9408_CR109","doi-asserted-by":"crossref","unstructured":"Visser, W., P\u0103s\u0103reanu, C., Pelanek, R.: Test input generation for Java containers using state matching. In: International Symposium on Software Testing and Analysis, pp. 37\u201348 (2006)","DOI":"10.1145\/1146238.1146243"},{"key":"9408_CR110","doi-asserted-by":"crossref","unstructured":"Xu, R.-G., Majumdar, R., Godefroid, P.: Testing for buffer overflows with length abstraction. In: International Symposium on Software Testing and Analysis, pp. 19\u201328 (2008)","DOI":"10.1145\/1390630.1390636"},{"key":"9408_CR111","unstructured":"Yang, J., Sar, C., Engler, D.: EXPLODE: a lightweight, general system for finding serious storage system errors. In: Operating System Design and Implementation, pp. 131\u2013146 (2006)"},{"key":"9408_CR112","unstructured":"Yang, J., Sar, C., Twohey, P., Cadar, C., Engler, D.: Automatically generating malicious disks using symbolic execution. In: IEEE Symposium on Security and Privacy, pp. 243\u2013257 (2006)"},{"key":"9408_CR113","unstructured":"Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. In: Operating System Design and Implementation, pp. 273\u2013288 (2004)"},{"key":"9408_CR114","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\/1993498.1993532"},{"issue":"2","key":"9408_CR115","doi-asserted-by":"crossref","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. Softw. Eng. 28(2), 183\u2013200 (2002)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9408-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-014-9408-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9408-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T15:11:40Z","timestamp":1565277100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-014-9408-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,18]]},"references-count":115,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["9408"],"URL":"https:\/\/doi.org\/10.1007\/s10472-014-9408-8","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,18]]}}}