{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:52:37Z","timestamp":1762458757180,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026577"},{"type":"electronic","value":"9783642026584"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02658-4_33","type":"book-chapter","created":{"date-parts":[[2009,6,22]],"date-time":"2009-06-22T11:00:16Z","timestamp":1245668416000},"page":"430-445","source":"Crossref","is-referenced-by-count":27,"title":["Generating and Analyzing Symbolic Traces of Simulink\/Stateflow Models"],"prefix":"10.1007","author":[{"given":"Aditya","family":"Kanade","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[]},{"given":"S.","family":"Ramesh","sequence":"additional","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]},{"given":"K. C.","family":"Shashidhar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","unstructured":"Simulink demos, http:\/\/www.mathworks.com\/products\/simulink\/demos.html"},{"key":"33_CR2","first-page":"43","volume":"109","author":"A. Agrawal","year":"2004","unstructured":"Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink\/Stateflow models to hybrid automata using graph transformations. ENTCS\u00a0109, 43\u201356 (2004)","journal-title":"ENTCS"},{"key":"33_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Kanade, A., Ramesh, S., Shashidhar, K.C.: Symbolic analysis for improving simulation coverage of Simulink\/Stateflow models. In: EMSOFT, pp. 89\u201398 (2008)","DOI":"10.1145\/1450058.1450071"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E. Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 365\u2013370. Springer, Heidelberg (2002)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-48983-5_8","volume-title":"Hybrid Systems: Computation and Control","author":"O. Bournez","year":"1999","unstructured":"Bournez, O., Maler, O., Pnueli, A.: Orthogonal polyhedra: Representation and computation. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, pp. 46\u201360. Springer, Heidelberg (1999)"},{"issue":"1","key":"33_CR7","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.scico.2006.03.009","volume":"64","author":"R. Claris\u00f3","year":"2007","unstructured":"Claris\u00f3, R., Cortadella, J.: The octahedron abstract domain. Science of Computer Programming\u00a064(1), 115\u2013139 (2007)","journal-title":"Science of Computer Programming"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-70930-5_6","volume-title":"Model-Driven Development of Reliable Automotive Services","author":"R. Cleaveland","year":"2008","unstructured":"Cleaveland, R., Smolka, S.A., Sims, S.: An instrumentation-based approach to controller model validation. In: Broy, M., Kr\u00fcger, I.H., Meisinger, M. (eds.) ASWSD 2006. LNCS, vol.\u00a04922, pp. 84\u201397. Springer, Heidelberg (2008)"},{"key":"33_CR9","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. of the Second International Symp. on Programming, pp. 106\u2013130 (1976)"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-71493-4_16","volume-title":"Hybrid Systems: Computation and Control","author":"A. Donz\u00e9","year":"2007","unstructured":"Donz\u00e9, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 174\u2013189. Springer, Heidelberg (2007)"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid Systems: Computation and Control","author":"A. Fehnker","year":"2004","unstructured":"Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 326\u2013341. Springer, Heidelberg (2004)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"HSCC","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol.\u00a02289, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"33_CR14","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.A. Gadkari","year":"2008","unstructured":"Gadkari, A.A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., Shashidhar, 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":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A. Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 291\u2013305. Springer, Heidelberg (2005)"},{"key":"33_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-78929-1_16","volume-title":"Hybrid Systems: Computation and Control","author":"A. Girard","year":"2008","unstructured":"Girard, A., Guernic, C.L.: Zonotope\/hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 215\u2013228. Springer, Heidelberg (2008)"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11730637_22","volume-title":"Hybrid Systems: Computation and Control","author":"A. Girard","year":"2006","unstructured":"Girard, A., Pappas, G.J.: Verification using simulation. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol.\u00a03927, pp. 272\u2013286. Springer, Heidelberg (2006)"},{"key":"33_CR18","unstructured":"GLPK (GNU Linear Programming Kit), http:\/\/www.gnu.org\/software\/glpk\/"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"issue":"2","key":"33_CR20","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Meth. in Sys. Design\u00a011(2), 157\u2013185 (1997)","journal-title":"Form. Meth. in Sys. Design"},{"key":"33_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.: HyTech: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 265\u2013293. Springer, Heidelberg (1995)"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-540-71493-4_27","volume-title":"Hybrid Systems: Computation and Control","author":"A. Agung Julius","year":"2007","unstructured":"Agung Julius, A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 329\u2013342. Springer, Heidelberg (2007)"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE, p. 310 (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"key":"33_CR24","unstructured":"Implementation of Qhull, http:\/\/www.qhull.org"},{"key":"33_CR25","unstructured":"Reactis, Reactive Systems, Inc., http:\/\/www.reactive-systems.com"},{"key":"33_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78800-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Dang, T., Ivancic, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 188\u2013202. Springer, Heidelberg (2008)"},{"key":"33_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"33_CR28","unstructured":"Simulink Design Verifier, The Mathworks, Inc., http:\/\/www.mathworks.com\/products\/sldesignverifier"},{"key":"33_CR29","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: FSE, pp. 263\u2013272 (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"33_CR30","unstructured":"Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verifying hybrid dynamic systems using CheckMate. In: ADPM (2000)"},{"key":"33_CR31","unstructured":"Simulink Reference, The Mathworks, Inc., http:\/\/www.mathworks.com"},{"key":"33_CR32","unstructured":"Safety Test Builder, TNI-Software, http:\/\/www.tni-software.com\/en\/produits\/safetytestbuilder"},{"key":"33_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/3-540-36580-X_35","volume-title":"Hybrid Systems: Computation and Control","author":"O. Stursberg","year":"2003","unstructured":"Stursberg, O., Krogh, B.H.: Efficient representation and computation of reachable sets for hybrid systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 482\u2013497. Springer, Heidelberg (2003)"},{"issue":"4","key":"33_CR34","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1145\/1113830.1113834","volume":"4","author":"S. Tripakis","year":"2005","unstructured":"Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embedded Comput. Syst.\u00a04(4), 779\u2013818 (2005)","journal-title":"ACM Trans. Embedded Comput. Syst."},{"key":"33_CR35","unstructured":"T-VEC Tester, T-VEC Technologies, Inc., http:\/\/www.t-vec.com\/solutions\/simulink.php"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02658-4_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T07:58:43Z","timestamp":1739174323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02658-4_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026577","9783642026584"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02658-4_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}