Formalization of Transform Methods using HOL Light


Algebraic techniques based on transform methods are widely used for solving differential equations and evaluating transfer function, and frequency response of signals while analyzing physical aspects of many safety-critical systems. To facilitate formal analysis of these systems, we present the formalization of transform methods (Laplace and Fourier transforms) using the multivariable calculus theories of HOL Light. In particular, we use integral, differential, transcendental and topological theories of multivariable calculus to formally define transform methods in higher-order logic and reason about the correctness of their properties, such as existence, linearity, frequency shifting, modulation, time scaling and differentiation and integration in time domain. In order to demonstrate the practical effectiveness of this formalization, we use it to formally verify some commonly used electrical circuits and an automobile suspension system.









  1. S.H. Taqdees and O. Hasan, Formally Verifying Transfer Functions of Linear Analog Circuits, IEEE Design and Test, 2017 (Accepted)
  2. A. Rashid and O. Hasan, On the Formalization of Fourier Transform in Higher-order Logic, Interactive Theorem Proving (ITP-16), Lecture Notes in Computer Science Volume 9807, 2016, Springer, pp. 483-490. (Rank A, CORE)
  3. S.H. Taqdees and O. Hasan, Formalization of Laplace Transform Using the Multivariate Calculus Theory of HOL-Light Logic for Programing Artificial Intelligence and Reasoning (LPAR 2013), Springer LNCS 8312, Stellenbosch, South Africa, pp. 744 – 758. (Rank A, CORE)
  4. S.H. Taqdees, Formalization of Laplace Transform using the Multivariable Calculus Theory of HOL-Light , Masters Thesis, National University of Sciences and Technology (NUST), Islamabad, Pakistan. 2013.