{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:08Z","timestamp":1740109088353,"version":"3.37.3"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>MATLAB\/Simulink is a popular toolset for developing embedded software. The main target of the toolset is numerical computing applications and the tools offer a rich language for manipulating matrices. This paper presents an approach to automatic, modular, contract-based verification of programs written in a subset of the MATLAB programming language. We focus on efficient handling of the built-in matrix manipulation functions commonly used in MATLAB. We restrict ourselves to the subset of MATLAB suitable for code generation, which means matrix types and shapes can be determined statically. We present an approach to static type and shape inference for matrices that is more strict than MATLAB, but aids verification. The type and shape information is then used in the verification. From the programs and contracts we generate verification conditions that are discharged with an off-the-shelf SMT solver. We discuss two approaches to encode matrix functions and evaluate them on a number of examples. We also investigate the use of k-induction to decrease the need for user annotations. We found our approach to be efficient for programs that manipulate relatively small matrices, which are common in embedded applications.<\/jats:p>","DOI":"10.1007\/s00165-015-0353-z","type":"journal-article","created":{"date-parts":[[2016,2,3]],"date-time":"2016-02-03T14:09:51Z","timestamp":1454508591000},"page":"79-107","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Contract-based verification of MATLAB-style matrix programs"],"prefix":"10.1145","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2859-6478","authenticated-orcid":false,"given":"Jonatan","family":"Wiik","sequence":"first","affiliation":[{"name":"Faculty of Science and Engineering, \u00c5bo Akademi University, Domkyrkotorget 3, 20500, \u00c5bo, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pontus","family":"Bostr\u00f6m","sequence":"additional","affiliation":[{"name":"Faculty of Science and Engineering, \u00c5bo Akademi University, Domkyrkotorget 3, 20500, \u00c5bo, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"20","volume-title":"TAP\u201914, vol 8570. LNCS","author":"Amin N","year":"2014"},{"issue":"5","key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1145\/543552.512564","article-title":"MaJIC: compiling MATLAB for speed and responsiveness","volume":"37","author":"Alm\u00e1si G","year":"2002","journal-title":"SIGPLAN Not"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barnett M Chang BYE Deline R Jacobs B Leino KRM (2006) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer FS Bonsangue MM Graf S de Roever W-P (eds) FMCO\u201905 vol 4111. LNCS. Springer Berlin pp 364\u2013387","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_2_1_2_6_2","first-page":"291","volume-title":"ICFEM\u201911, vol 6991. LNCS","author":"Bostr\u00f6m P","year":"2011"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bostr\u00f6m P Wiik J (2015) Contract-based verification of discrete-time multi-rate Simulink models. Softw Syst Model. doi:10.1007\/s10270-015-0477-x","DOI":"10.1007\/s10270-015-0477-x"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Jay CCB Steckler P (1998) The functional imperative: Shape! In: Hankin C (ed) ESOP\u201998 vol 1381. LNCS. Springer Berlin pp 139\u2013153","DOI":"10.1007\/BFb0053568"},{"key":"e_1_2_1_2_9_2","first-page":"233","volume-title":"SEFM\u201912, vol 7504. LNCS","author":"Cuoq P","year":"2012"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Chalin P Kiniry JR Leavens GT Poll E (2006) Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: de Boer FS Bonsangue MM Graf S de Roever W-P (eds) FMCO\u201906 vol 4111. LNCS. Springer Berlin pp 342\u2013363","DOI":"10.1007\/11804192_16"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"de Moura L Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR Rehof J (eds) TACAS\u201908 vol 4963. LNCS. Springer Berlin pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_13_2","first-page":"351","volume-title":"SAS\u201911, vol 6887. LNCS","author":"Donaldson AF","year":"2011"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"de Moura L Bj\u00f8rner N (2009) Generalized efficient array decision procedures. In: FMCAD\u201909. IEEE New York pp 45\u201352","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"2","key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1145\/316686.316693","article-title":"Techniques for the translation of MATLAB programs into Fortran 90","volume":"21","author":"de Rose L","year":"1999","journal-title":"ACM TOPLAS"},{"key":"e_1_2_1_2_16_2","first-page":"10","volume-title":"FoVeOOS\u201910, vol 6528. LNCS","author":"F\u00e4hndrich M","year":"2011"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90144-7"},{"key":"e_1_2_1_2_18_2","first-page":"125","volume-title":"ESOP\u201913, vol 7792, LNCS","author":"Filliatre JC","year":"2013"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Ge Y de Moura L (2009) Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani A Maler O (eds) CAV\u201909 vol 5643. LNCS. Springer Berlin pp 306\u2013320","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_2_1_2_20_2","first-page":"139","volume-title":"NFM\u201913, vol 7871. LNCS","author":"Garoche PL","year":"2013"},{"key":"e_1_2_1_2_21_2","first-page":"163","volume-title":"VMCAI\u201910, vol 5944. LNCS","author":"Henzinger TA","year":"2010"},{"issue":"5","key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","first-page":"848","DOI":"10.1145\/1152649.1152651","article-title":"An algebraic array shape inference system for MATLAB","volume":"28","author":"Joisha PG","year":"2006","journal-title":"ACM TOPLAS"},{"volume-title":"Viper: a verification infrastructure for permission-based reasoning","year":"2014","author":"Juhasz U","key":"e_1_2_1_2_23_2"},{"key":"e_1_2_1_2_24_2","first-page":"348","volume-title":"LPAR\u201910, vol 6355. LNCS","author":"Leino KRM","year":"2010"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Monahan R (2009) Reasoning about comprehensions with first-order SMT-solvers. In: SAC\u201909. ACM New York pp 615\u2013622","DOI":"10.1145\/1529282.1529411"},{"key":"e_1_2_1_2_26_2","unstructured":"Mathworks Inc. (2014) Simulink. http:\/\/www.mathworks.com"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_2_28_2","first-page":"80","volume-title":"VMCAI\u201915, vol 8931. LNCS","author":"Reynolds A","year":"2015"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_2_30_2","first-page":"298","volume-title":"SAS\u201911, vol 6887. LNCS","author":"Suter P","year":"2011"},{"key":"e_1_2_1_2_31_2","first-page":"89","volume-title":"APLAS\u201911, vol 7078. LNCS","author":"Traytel D","year":"2011"},{"key":"e_1_2_1_2_32_2","first-page":"396","volume-title":"ICFEM\u201914, vol 8829. LNCS","author":"Wiik J","year":"2014"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-11737-9_26","volume-title":"Contract-based verification of MATLAB and Simulink matrix-manipulating code","author":"Wiik J","year":"2014"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Xi H (1999) Dependent types in practical programming. In: POPL\u201999. ACM New York pp 214\u2013227","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0353-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0353-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0353-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:18:07Z","timestamp":1641485887000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0353-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["10.1007\/s00165-015-0353-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0353-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,3]]}}}