Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Mathematical Modeling: Problem Solving01:29

Mathematical Modeling: Problem Solving

76
Mathematical modeling transforms real-world scenarios into mathematical expressions, allowing for structured problem-solving and analysis. This process involves defining the situation, assigning variables to measurable quantities, selecting an appropriate model, and solving the resulting equation. Such models are invaluable in finance, providing precise methods to evaluate investments, loans, and repayment structures.A widely used example is the calculation of fixed monthly payments on a loan,...
76
Introduction to MATLAB01:24

Introduction to MATLAB

431
MATLAB stands for Matrix Laboratory. MathWorks developed MATLAB as a multi-paradigm numerical computing environment and proprietary programming language. It has evolved significantly over the years to become a tool utilized by engineers, scientists, and mathematicians for various tasks, including matrix calculations, developing algorithms, data analysis, and visualization. MATLAB's applications span various industries and disciplines. It's used in image and signal processing,...
431
Theorems of Pappus and Guldinus: Problem Solving01:12

Theorems of Pappus and Guldinus: Problem Solving

892
Pappus and Guldinus's theorems are powerful mathematical principles that are used for finding the surface area and volume of composite shapes. For example, consider a cylindrical storage tank with a conical top. Finding the surface area or volume can be challenging for such complex shapes. These theorems are particularly useful in calculating the volume and surface area of such systems. Here, the cylindrical storage tank with a conical top can be broken down into two simple shapes: a...
892
Relation between Mathematical Equations and Block Diagrams01:20

Relation between Mathematical Equations and Block Diagrams

2.5K
In a spring-mass-damper system, the second-order differential equation describes the dynamic behavior of the system. When transformed into the Laplace domain under zero initial conditions, this equation can be effectively analyzed and manipulated. The transformation into the Laplace domain converts differential equations into algebraic equations, simplifying the process of isolating the output.
2.5K
Fundamental Theorem of Algebra01:30

Fundamental Theorem of Algebra

46
The Fundamental Theorem of Algebra is central to the study of polynomial equations, asserting that every non-constant polynomial with complex coefficients has at least one complex zero. This means that a polynomial of degree n ≥ 1, written as:  with an ≠ 0, has at least one solution in the complex number system. Since the set of real numbers is a subset of complex numbers, this theorem applies equally to polynomials with real coefficients.Building on this result, the Complete...
46
Thevinin's Theorem01:15

Thevinin's Theorem

1.1K
Thévenin's theorem plays a pivotal role in electrical circuit analysis, offering a solution to the challenges posed by variable loads within a circuit. In practical applications, it is common to encounter circuits where certain elements remain fixed while others fluctuate, often referred to as the "load." A typical household electrical outlet serves as a prime example of a variable load, as it can be connected to a variety of appliances, each with its own unique electrical characteristics.
1.1K

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

Formal Verification of Deep Brain Stimulation Controllers for Parkinson's Disease Treatment.

Neural computation·2023
Same author

Formalization of bond graph using higher-order-logic theorem proving.

ISA transactions·2022
Same author

Chronic kidney disease diagnosis using decision tree algorithms.

BMC nephrology·2021
Same author

How childhood diseases awareness contributes to minimize the risk of disease severity in children under five age: An evolutionary study.

JPMA. The Journal of the Pakistan Medical Association·2021
Same author

Formal reasoning about synthetic biology using higher-order-logic theorem proving.

IET systems biology·2020
Same author

Stunting diagnostic and awareness: impact assessment study of sociodemographic factors of stunting among school-going children of Pakistan.

BMC pediatrics·2020
Same journal

DARUMA: a gateway to fast and easy prediction of intrinsically disordered regions.

PeerJ. Computer science·2026
Same journal

Alzheimer's disease detection using a quantum deep neural network with Haralick feature extraction and simulated annealing optimization.

PeerJ. Computer science·2026
Same journal

Network anomaly detection using Deep Autoencoder and parallel Artificial Bee Colony algorithm-trained neural network.

PeerJ. Computer science·2026
Same journal

An anomaly detection model for multivariate time series with anomaly perception.

PeerJ. Computer science·2026
Same journal

Retraction: A wormhole attack detection method for tactical wireless sensor networks.

PeerJ. Computer science·2026
Same journal

Evaluation of mental disorder with prioritization of its type by utilizing the bipolar complex fuzzy decision-making approach based on Schweizer-Sklar prioritized aggregation operators.

PeerJ. Computer science·2026
See all related articles

Related Experiment Video

Updated: Nov 9, 2025

Author Spotlight: An Optimized Automated Method for Investigating Retinoic Acid Receptors in Neuronal Mitochondria
08:33

Author Spotlight: An Optimized Automated Method for Investigating Retinoic Acid Receptors in Neuronal Mitochondria

Published on: July 28, 2023

765

Formal verification of Matrix based MATLAB models using interactive theorem proving.

Ayesha Gauhar1, Adnan Rashid1, Osman Hasan1

  • 1School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan.

Peerj. Computer Science
|April 9, 2021
PubMed
Summary
This summary is machine-generated.

This study introduces a library and translator for converting MATLAB models to higher-order logic, enabling formal verification of complex systems. This approach enhances model analysis beyond traditional simulation methods.

Keywords:
Formal MethodsFormal verificationHOL LightHigher-order logicInteractive theorem provingMATLABMatrix based MATLAB models

More Related Videos

2D and 3D Matrices to Study Linear Invadosome Formation and Activity
12:25

2D and 3D Matrices to Study Linear Invadosome Formation and Activity

Published on: June 2, 2017

10.2K
Interactive and Visualized Online Experimentation System for Engineering Education and Research
08:35

Interactive and Visualized Online Experimentation System for Engineering Education and Research

Published on: November 24, 2021

2.7K

Related Experiment Videos

Last Updated: Nov 9, 2025

Author Spotlight: An Optimized Automated Method for Investigating Retinoic Acid Receptors in Neuronal Mitochondria
08:33

Author Spotlight: An Optimized Automated Method for Investigating Retinoic Acid Receptors in Neuronal Mitochondria

Published on: July 28, 2023

765
2D and 3D Matrices to Study Linear Invadosome Formation and Activity
12:25

2D and 3D Matrices to Study Linear Invadosome Formation and Activity

Published on: June 2, 2017

10.2K
Interactive and Visualized Online Experimentation System for Engineering Education and Research
08:35

Interactive and Visualized Online Experimentation System for Engineering Education and Research

Published on: November 24, 2021

2.7K

Area of Science:

  • Computer Science
  • Electrical Engineering
  • Formal Methods

Background:

  • MATLAB is a widely used high-level programming language for modeling and analyzing systems in engineering and science.
  • Traditional analysis methods like simulation and debugging offer limited coverage due to inherent incompleteness.
  • Formal verification offers enhanced coverage but requires challenging and time-consuming development of formal models, especially for higher-order-logic models.

Purpose of the Study:

  • To facilitate the formal verification of MATLAB models by reducing the effort required to develop formal models.
  • To present a library of higher-order-logic functions for common MATLAB matrix functions.
  • To introduce a translator for automatic conversion of MATLAB models to higher-order logic.

Main Methods:

  • Developed a library of higher-order-logic functions mirroring commonly used MATLAB matrix functions.
  • Created a translator for automatic conversion of MATLAB models into higher-order logic representations.
  • Utilized the HOL Light theorem prover for formal verification of the converted models.

Main Results:

  • Successfully created a library of higher-order-logic functions and an automatic translator for MATLAB models.
  • Demonstrated the approach by formally analyzing a Finite Impulse Response (FIR) filter model.
  • The formal models were successfully verified within the HOL Light theorem prover.

Conclusions:

  • The proposed library and translator significantly simplify the process of formally verifying MATLAB models.
  • This approach overcomes the limitations of traditional simulation and debugging methods.
  • Enables rigorous formal analysis of complex systems modeled in MATLAB, enhancing reliability and correctness.