{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:54:25Z","timestamp":1725807265851},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319117362"},{"type":"electronic","value":"9783319117379"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_26","type":"book-chapter","created":{"date-parts":[[2014,10,15]],"date-time":"2014-10-15T00:52:14Z","timestamp":1413334334000},"page":"396-412","source":"Crossref","is-referenced-by-count":6,"title":["Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code"],"prefix":"10.1007","author":[{"given":"Jonatan","family":"Wiik","sequence":"first","affiliation":[]},{"given":"Pontus","family":"Bostr\u00f6m","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Alm\u00e1si, G., Padua, D.: MaJIC: Compiling MATLAB for speed and responsiveness. SIGPLAN Not.\u00a037(5) (2002)","DOI":"10.1145\/543552.512564"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R. M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: The Spec# experience. Commun. ACM\u00a054(6) (2011)","DOI":"10.1145\/1953122.1953145"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-24559-6_21","volume-title":"Formal Methods and Software Engineering","author":"P. Bostr\u00f6m","year":"2011","unstructured":"Bostr\u00f6m, P.: Contract-based verification of simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 291\u2013306. Springer, Heidelberg (2011)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-75292-9_6","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"P. Bostr\u00f6m","year":"2007","unstructured":"Bostr\u00f6m, P., Morel, L., Wald\u00e9n, M.: Stepwise development of simulink models using the refinement calculus framework. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol.\u00a04711, pp. 79\u201393. Springer, Heidelberg (2007)"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0053568","volume-title":"Programming Languages and Systems","author":"C.B. Jay","year":"1998","unstructured":"Jay, C.B., Steckler, P.A.: The functional imperative: Shape! In: Hankin, C. (ed.) ESOP 1998. LNCS, vol.\u00a01381, p. 139. Springer, Heidelberg (1998)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM\u00a054 (2011)","DOI":"10.1145\/1941487.1941509"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M. F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 10\u201330. Springer, Heidelberg (2011)"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Joisha, P.G., Banerjee, P.: An algebraic array shape inference system for MATLAB. ACM TOPLAS\u00a028(5) (2006)","DOI":"10.1145\/1152649.1152651"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT-solvers. In: SAC 2009. ACM (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. System Sci.\u00a017 (1978)","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bjorner, N.: Generalized, efficient array decision procedures. In: FMCAD 2009. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"26_CR15","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"de Rose, L., Padua, D.: Techniques for the translation of MATLAB programs into Fortran 90. ACM TOPLAS\u00a021(2) (1999)","DOI":"10.1145\/316686.316693"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Wiik, J., Bostr\u00f6m, P.: Contract-based verification of MATLAB and Simulink matrix-manipulating code. Tech. Rep. 1107, TUCS (2014)","DOI":"10.1007\/978-3-319-11737-9_26"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Xi, H.: Dependent ML: An approach to practical programming with dependent types. J. Funct. Programming\u00a017(2) (2007)","DOI":"10.1017\/S0956796806006216"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T04:29:42Z","timestamp":1559017782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}