{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T10:59:42Z","timestamp":1762340382417,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642170706"},{"type":"electronic","value":"9783642170713"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-17071-3_11","type":"book-chapter","created":{"date-parts":[[2010,11,11]],"date-time":"2010-11-11T07:12:58Z","timestamp":1289459578000},"page":"208-227","source":"Crossref","is-referenced-by-count":43,"title":["Mutation-Based Test Case Generation for Simulink Models"],"prefix":"10.1007","author":[{"given":"Angelo","family":"Brillout","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nannan","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Mazzucchi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mitra","family":"Purandare","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-540-70545-1_19","volume-title":"Computer Aided Verification","author":"A. Gadkari","year":"2008","unstructured":"Gadkari, A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., Shashidar, K.C.: AutoMOTGen: Automatic model oriented test generator for embedded control systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 204\u2013208. Springer, Heidelberg (2008)"},{"key":"11_CR3","first-page":"368","volume-title":"Design Automation Conference (DAC)","author":"D. Kroening","year":"2003","unstructured":"Kroening, D., Clarke, E.M., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conference (DAC), pp. 368\u2013371. ACM, New York (2003)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-70545-1_20","volume-title":"Computer Aided Verification","author":"A. Holzer","year":"2008","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: FShell: Systematic test case generation for dynamic analysis and measurement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 209\u2013213. Springer, Heidelberg (2008)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-04772-5_38","volume-title":"Computer Aided Systems Theory - EUROCAST 2009","author":"D. Angeletti","year":"2009","unstructured":"Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Automatic test generation for coverage analysis using CBMC. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) Computer Aided Systems Theory - EUROCAST 2009. LNCS, vol.\u00a05717, pp. 287\u2013294. Springer, Heidelberg (2009)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-93900-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Holzer","year":"2009","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 151\u2013166. Springer, Heidelberg (2009)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11561163_1","volume-title":"Formal Methods for Components and Objects","author":"T. Ball","year":"2005","unstructured":"Ball, T.: A theory of predicate-complete test coverage and generation. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol.\u00a03657, pp. 1\u201322. Springer, Heidelberg (2005)"},{"key":"11_CR8","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 (ICSE), pp. 326\u2013335 (2004)","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"11_CR9","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Transactions on Software Engineering, TSE (2010)"},{"key":"11_CR10","first-page":"1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"O. Kupferman","year":"2008","unstructured":"Kupferman, O., Li, W., Seshia, S.A.: A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 1\u20139. IEEE, Los Alamitos (2008)"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1109\/TSE.2006.37","volume":"32","author":"J.R. Ruthruff","year":"2006","unstructured":"Ruthruff, J.R., Burnett, M.M., Rothermel, G.: Interactive fault localization techniques in a spreadsheet environment. IEEE Transactions on Software Engineering (TSE)\u00a032, 213\u2013239 (2006)","journal-title":"IEEE Transactions on Software Engineering (TSE)"},{"key":"11_CR12","first-page":"69","volume-title":"International Symposium on Software Testing and Analysis (ISSTA)","author":"D. Schuler","year":"2009","unstructured":"Schuler, D., Dallmeier, V., Zeller, A.: Efficient mutation testing by checking invariant violations. In: International Symposium on Software Testing and Analysis (ISSTA), pp. 69\u201380. ACM, New York (2009)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/11901433_33","volume-title":"Formal Methods and Software Engineering","author":"B. Meenakshi","year":"2006","unstructured":"Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 606\u2013620. Springer, Heidelberg (2006)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-30476-0_23","volume-title":"Automated Technology for Verification and Analysis","author":"A. Fehnker","year":"2004","unstructured":"Fehnker, A., Krogh, B.H.: Hybrid system verification is not a sinecure: The electronic throttle control case study. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 263\u2013277. Springer, Heidelberg (2004)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/11563228_10","volume-title":"Computer Safety, Reliability, and Security","author":"A. Joshi","year":"2005","unstructured":"Joshi, A., Heimdahl, M.P.E.: Model-based safety analysis of Simulink models using SCADE design verifier. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol.\u00a03688, pp. 122\u2013135. Springer, Heidelberg (2005)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-02658-4_57","volume-title":"Computer Aided Verification","author":"M. Ryabtsev","year":"2009","unstructured":"Ryabtsev, M., Strichman, O.: Translation validation: From simulink to c. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol.\u00a05643, pp. 696\u2013701. Springer, Heidelberg (2009)"},{"key":"11_CR17","unstructured":"The Mathworks: Simulink design verifier user\u2019s guide. version 1.5 (2009), \n                    \n                      http:\/\/www.mathworks.com\/access\/helpdesk\/help\/toolbox\/sldv\/"},{"key":"11_CR18","first-page":"69","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"A. Brillout","year":"2009","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 69\u201376. IEEE, Los Alamitos (2009)"},{"key":"11_CR19","series-title":"Kluwer International Series in Engineering and Computer Science Series","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-1-4615-0817-5_13","volume-title":"Logic Synthesis and Verification","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., van Eijk, C.A.J.: Combinational and sequential equivalence checking. In: Logic Synthesis and Verification. Kluwer International Series in Engineering and Computer Science Series, pp. 343\u2013372. Kluwer, Norwell (2002)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"11_CR21","first-page":"66","volume-title":"IEEE\/ACM International Conference on Computer-Aided Design","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Clarke, E.: Checking consistency of C and Verilog using predicate abstraction and induction. In: IEEE\/ACM International Conference on Computer-Aided Design, pp. 66\u201372. IEEE, Los Alamitos (2004)"},{"key":"11_CR22","unstructured":"Victor, A.C.: Interpretation of IEEE-854 floating-point standard and definition in the HOL system. Technical report, NASA Langley (1995)"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1022973506233","volume":"22","author":"J. Harrison","year":"2003","unstructured":"Harrison, J.: Formal verification of square root algorithms. Formal Methods in System Design (FMSD)\u00a022, 143\u2013153 (2003)","journal-title":"Formal Methods in System Design (FMSD)"},{"key":"11_CR24","first-page":"196","volume-title":"Programming Language Design and Implementation (PLDI)","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), pp. 196\u2013207. ACM, New York (2003)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"11_CR26","volume-title":"Decision Procedures","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","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":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"11_CR29","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a035, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"11_CR31","volume-title":"Design Automation Conference (DAC)","author":"H. Chockler","year":"2010","unstructured":"Chockler, H., Kroening, D., Purandare, M.: Coverage in interpolation-based model checking. In: Design Automation Conference (DAC), ACM, New York (2010)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17071-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T00:53:53Z","timestamp":1553216033000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17071-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642170706","9783642170713"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17071-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}