Skip to main content
SpringerLink
Log in

Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8829))

Included in the following conference series:

Abstract

This paper presents an approach to automatic, modular, contract-based verification of programs written in a subset of the MATLAB programming language, with focus on efficiently handling the provided matrix manipulation functions. We statically infer types and shapes for matrices in the language and use this information in the verification. We consider two approaches for verification: direct axiomatisation of the built-in matrix functions and expansion of the functions. We evaluate our approaches on a number of examples and discuss challenges for automatic verification in this setting.

Work done in the EFFIMA program coordinated by Fimecc and the EDiHy project funded by the Academy of Finland.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Almási, G., Padua, D.: MaJIC: Compiling MATLAB for speed and responsiveness. SIGPLAN Not. 37(5) (2002)

    Google Scholar 

  2. 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. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: The Spec# experience. Commun. ACM 54(6) (2011)

    Google Scholar 

  4. Boström, P.: Contract-based verification of simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 291–306. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Boström, P., Morel, L., Waldén, M.: Stepwise development of simulink models using the refinement calculus framework. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 79–93. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Jay, C.B., Steckler, P.A.: The functional imperative: Shape! In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, p. 139. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. 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. 4111, pp. 342–363. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54 (2011)

    Google Scholar 

  9. de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Joisha, P.G., Banerjee, P.: An algebraic array shape inference system for MATLAB. ACM TOPLAS 28(5) (2006)

    Google Scholar 

  12. Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT-solvers. In: SAC 2009. ACM (2009)

    Google Scholar 

  13. Milner, R.: A theory of type polymorphism in programming. J. Comput. System Sci. 17 (1978)

    Google Scholar 

  14. de Moura, L., Bjorner, N.: Generalized, efficient array decision procedures. In: FMCAD 2009. IEEE (2009)

    Google Scholar 

  15. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  16. de Rose, L., Padua, D.: Techniques for the translation of MATLAB programs into Fortran 90. ACM TOPLAS 21(2) (1999)

    Google Scholar 

  17. Wiik, J., Boström, P.: Contract-based verification of MATLAB and Simulink matrix-manipulating code. Tech. Rep. 1107, TUCS (2014)

    Google Scholar 

  18. Xi, H.: Dependent ML: An approach to practical programming with dependent types. J. Funct. Programming 17(2) (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Information Technologies, Åbo Akademi University, Finland

    Jonatan Wiik & Pontus Boström

Authors
  1. Jonatan Wiik
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pontus Boström
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Inria Nancy - Grand Est, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy, France

    Stephan Merz

  2. Université du Luxembourg, 6 rue Richard Coudenhove-Kalergi, 1359, Luxembourg, Luxembourg

    Jun Pang

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Wiik, J., Boström, P. (2014). Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11737-9_26

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11736-2

  • Online ISBN: 978-3-319-11737-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation