{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T09:49:28Z","timestamp":1725702568698},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340253"},{"type":"electronic","value":"9783642340260"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34026-0_35","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T21:07:20Z","timestamp":1348607240000},"page":"474-487","source":"Crossref","is-referenced-by-count":1,"title":["Model-Based Static Code Analysis for MATLAB Models"],"prefix":"10.1007","author":[{"given":"Zheng","family":"Lu","sequence":"first","affiliation":[]},{"given":"Supratik","family":"Mukhopadhyay","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","unstructured":"http:\/\/www.omg.org\/mda\/"},{"key":"35_CR2","unstructured":"http:\/\/www.omg.org\/spec\/UML\/2.0\/"},{"key":"35_CR3","unstructured":"http:\/\/www.ni.com\/labview\/"},{"key":"35_CR4","unstructured":"http:\/\/www.mathworks.com\/products\/matlab\/"},{"key":"35_CR5","unstructured":"Polyspace, \n                    \n                      http:\/\/www.mathworks.com\/products\/polyspace\/"},{"key":"35_CR6","unstructured":"http:\/\/www.vectorcast.com"},{"key":"35_CR7","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, pp. 238\u2013252. ACM, New York (1977)"},{"key":"35_CR8","unstructured":"Gomes, I., Morgado, P., Gomes, T., Moreira, R.: An overview on the static code analysis approach in software development. Tech. rep., Faculdade de Engenharia da Universidade do Porto (2009)"},{"key":"35_CR9","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), \n                    \n                      http:\/\/www.SMT-LIB.org"},{"key":"35_CR10","unstructured":"Dutertre, B., Moura, L.D.: The yices smt solver. Tech. rep. (2006)"},{"key":"35_CR11","unstructured":"http:\/\/www.ilovematlab.cn\/forum.php"},{"key":"35_CR12","volume-title":"Software testing techniques","author":"B. Beizer","year":"1990","unstructured":"Beizer, B.: Software testing techniques, 2nd edn. Van Nostrand Reinhold Co., New York (1990)","edition":"2"},{"key":"35_CR13","unstructured":"Woldman, K.I.: A dual programming approach to software testing. Master\u2019s thesis, Santa Clara University (1992)"},{"key":"35_CR14","volume-title":"Practical Software Testing","author":"J.-F. Collard","year":"2002","unstructured":"Collard, J.-F., Burnstein, I.: Practical Software Testing. Springer-Verlag New York, Inc., Secaucus (2002)"},{"key":"35_CR15","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-642-61455-2_16","volume-title":"Proceedings of the NATO Advanced Study Institute on Deductive Program Design","author":"E. Clarke","year":"1996","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking. In: Proceedings of the NATO Advanced Study Institute on Deductive Program Design, pp. 305\u2013349. Springer-Verlag New York, Inc., Secaucus (1996)"},{"key":"35_CR16","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.-L. Chang","year":"1997","unstructured":"Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving, 1st edn. Academic Press, Inc., Orlando (1997)","edition":"1"},{"key":"35_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus (1999)"},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45657-0_1","volume-title":"Computer Aided Verification","author":"G.J. Holzmann","year":"2002","unstructured":"Holzmann, G.J.: Software Analysis and Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 1\u201316. Springer, Heidelberg (2002)"},{"key":"35_CR19","doi-asserted-by":"crossref","unstructured":"Evans, D., Guttag, J., Horning, J., Tan, Y.: Lclint: A tool for using specifications to check code. In: ACM SIGSOFT Software Engineering Notes, vol.\u00a019, pp. 87\u201396. ACM (1994)","DOI":"10.1145\/195274.195297"},{"issue":"4","key":"35_CR20","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MS.2003.1207453","volume":"20","author":"P. Anderson","year":"2003","unstructured":"Anderson, P., Reps, T.W., Teitelbaum, T., Zarins, M.: Tool support for fine-grained software inspection. IEEE Software\u00a020(4), 42\u201350 (2003)","journal-title":"IEEE Software"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"Evans, D., Guttag, J., Horning, J., Tan, Y.M.: Lclint: A tool for using specifications to check code. In: ACM SIGSOFT Software Engineering Notes, vol.\u00a019, pp. 87\u201396. ACM (1994)","DOI":"10.1145\/195274.195297"},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: Esp: Path-sensitive program verification in polynomial time. In: PLDI, pp. 57\u201368 (2002)","DOI":"10.1145\/543552.512538"},{"issue":"1","key":"35_CR23","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/s100090050017","volume":"2","author":"F. Martin","year":"1998","unstructured":"Martin, F.: PAG \u2013 an efficient program analyzer generator. International Journal on Software Tools for Technology Transfer\u00a02(1), 46\u201367 (1998)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 69\u201382. ACM Press (2002)","DOI":"10.1145\/512529.512539"},{"key":"35_CR25","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 157\u2013185 (1997)","DOI":"10.1023\/A:1008678014487"},{"key":"35_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/3-540-44898-5_20","volume-title":"Static Analysis","author":"N. Halbwachs","year":"2003","unstructured":"Halbwachs, N., Merchat, D., Parent-vigouroux, C.: Cartesian Factoring of Polyhedra in Linear Relation Analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 355\u2013365. Springer, Heidelberg (2003)"},{"issue":"2","key":"35_CR27","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.tcs.2005.11.026","volume":"354","author":"R. Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivancic, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci.\u00a0354(2), 250\u2013271 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"35_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0054172","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Aiken","year":"1998","unstructured":"Aiken, A., F\u00e4hndrich, M., Su, Z.: Detecting Races in Relay Ladder Logic Programs. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 184\u2013200. Springer, Heidelberg (1998)"},{"key":"35_CR29","doi-asserted-by":"crossref","unstructured":"Lam, M.S., Whaley, J., Livshits, V.B., Martin, M.C., Avots, D., Carbin, M., Unkel, C.: Context-sensitive program analysis as database queries. In: PODS, pp. 1\u201312 (2005)","DOI":"10.1145\/1065167.1065169"},{"key":"35_CR30","unstructured":"http:\/\/www.cs.cornell.edu\/talc\/"},{"issue":"4","key":"35_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.10.024","volume":"127","author":"M.E. Beato","year":"2005","unstructured":"Beato, M.E., Barrio-Sol\u00f3rzano, M., Cuesta, C.E., de la Fuente, P.: Uml automatic verification tool with formal methods. Electron. Notes Theor. Comput. Sci.\u00a0127(4), 3\u201316 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"35_CR32","unstructured":"http:\/\/www.cs.cmu.edu\/~modelcheck\/smv.html"},{"key":"35_CR33","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1145\/2048066.2048077","volume-title":"Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2011","author":"J. Doherty","year":"2011","unstructured":"Doherty, J., Hendren, L., Radpour, S.: Kind analysis for matlab. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2011, pp. 99\u2013118. ACM, New York (2011)"},{"issue":"2","key":"35_CR34","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/570406.570408","volume":"31","author":"P.G. Joisha","year":"2000","unstructured":"Joisha, P.G., Banerjee, P.: Correctly detecting intrinsic type errors in typeless languages such as matlab. SIGAPL APL Quote Quad\u00a031(2), 7\u201321 (2000)","journal-title":"SIGAPL APL Quote Quad"},{"key":"35_CR35","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1637837.1637851","volume-title":"Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2009","author":"M. Kaufmann","year":"2009","unstructured":"Kaufmann, M., Kornerup, J., Reitblatt, M.: Formal verification of labview programs using the acl2 theorem prover. In: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2009, pp. 82\u201389. ACM, New York (2009)"},{"key":"35_CR36","unstructured":"http:\/\/www.cs.utexas.edu\/~moore\/acl2\/"},{"key":"35_CR37","unstructured":"Softcheck, \n                    \n                      http:\/\/www.sofcheck.com\/products\/inspector.html"},{"issue":"5","key":"35_CR38","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/MS.2008.130","volume":"25","author":"N. Ayewah","year":"2008","unstructured":"Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Using static analysis to find bugs. IEEE Software\u00a025(5), 22\u201329 (2008)","journal-title":"IEEE Software"},{"key":"35_CR39","unstructured":"Fortify, \n                    \n                      http:\/\/www.fortify.com\/"},{"key":"35_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/3-540-47764-0_25","volume-title":"Static Analysis","author":"D. Wagner","year":"2001","unstructured":"Wagner, D.: Static Analysis and Software Assurance. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, p. 431. Springer, Heidelberg (2001)"},{"key":"35_CR41","unstructured":"Klock source code analysis for android platform, \n                    \n                      http:\/\/www.klocwork.com\/news\/press-releases\/releases\/2008\/PR-2008_11_11-Source-code-analysis-for-Android.php"},{"key":"35_CR42","unstructured":"Jif: java information flow, \n                    \n                      http:\/\/www.cs.cornell.edu\/jif\/"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34026-0_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T08:41:23Z","timestamp":1620117683000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34026-0_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340253","9783642340260"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34026-0_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}