On the Formalization of Fourier Transform in Higher-order Logic

Adnan Rashid

Fourier transform based techniques are widely used for solving differential equations and to perform the frequency response analysis of signals in many safety-critical systems. To perform the formal analysis of these systems, we present a formalization of Fourier transform using higher-order logic. In particular, we use the HOL-Light's differential, integral, transcendental and topological theories of multivariable calculus to formally define Fourier transform and reason about the correctness of its classical properties, such as existence, linearity, frequency shifting, modulation, time reversal and differentiation in time-domain. In order to demonstrate the practical effectiveness of the proposed formalization, we use it to formally verify the frequency response of an automobile suspension system.

Case Study

Automobile Suspension System

Proof Script

Contact Information

Adnan Rashid is a PhD student at NUST School of Electrical Engineering & Computer Science. He is working on his PhD thesis in the System Analysis & Verification (SAVe) Lab of NUST-SEECS, under the supervision of Dr. Osman Hasan.