Contract-based verification of MATLAB-style matrix programs

DOI10.1007/s00165-015-0353-zzbMath1338.65116OpenAlexW2340067148MaRDI QIDQ282101

Jonatan Wiik, Pontus Boström

Publication date: 12 May 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-015-0353-z

zbMATH Keywords

programming languageMatlabmatrix functionautomated verificationnumerical computingSMT solving

Mathematics Subject Classification ID

Related Items (3)

Contract-based verification of MATLAB-style matrix programs ⋮ A contract-based semantics and refinement for Simulink ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

Uses Software

• Dafny
• Matlab
• ML
• MaJIC
• Simulink
• Why3
• JML
• Spec#
• Frama-C
• z3
• Boogie
• CVC4
• WhyML
• Viper

Cites Work

• Contract-based verification of MATLAB-style matrix programs
• Type inference with subtypes
• A theory of type polymorphism in programming
• Dafny: An Automatic Program Verifier for Functional Correctness
• Static Contract Checking with Abstract Interpretation
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Invariant and Type Inference for Matrices
• Induction for SMT Solvers
• Dependent ML An approach to practical programming with dependent types
• Why3 — Where Programs Meet Provers
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Contract-based verification of MATLAB-style matrix programs