
MATLAB is widely used in scientific, engineering, and numerical computations. Complex systems such as digital signal processors, process control systems, etc. are modeled in MATLAB and analyzed; C implementation of the system can be automatically generated from the validated MATLAB model. We combine static analysis techniques with model-based deductive verification using SMT solvers to provide a framework to analyze MATLAB code. The analyzer is generated by translating the collecting semantics of a MATLAB script to a formula in first order logic over multiple underlying theories. Function calls in a script can be handled by importing SMT assertions obtained by analyzing MATLAB files containing function definitions. Logical specification of the desired program behavior (rather its negation) is incorporated as a first order logic formula. An SMT-LIB formula solver treats the combined formula as a "constraint" and "solves" it. The "solved form" can be used to identify logical errors in the MATLAB model.
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
