The Formalization of Discrete Fourier Transform in HOL
Traditionally, Discrete Fourier Transform (DFT) is performed with numerical or symbolic computation, which cannot guarantee 100% accurate analysis which may be necessary for safety-critical applications. Machine theorem proving is one of the formal methods that perform accurate analysis with complet...
Main Authors: | Zhiping Shi, Yupeng Zhang, Yong Guan, Liming Li, Jie Zhang |
---|---|
Format: | Article |
Language: | English |
Published: |
Hindawi Limited
2015-01-01
|
Series: | Mathematical Problems in Engineering |
Online Access: | http://dx.doi.org/10.1155/2015/687152 |
Similar Items
-
Formalization of Function Matrix Theory in HOL
by: Zhiping Shi, et al.
Published: (2014-01-01) -
Formalization of Matrix Theory in HOL4
by: Zhiping Shi, et al.
Published: (2014-08-01) -
Formalization of Discrete-time Markov Chains in HOL
by: Liu, Liya
Published: (2013) -
The Gauge Integral Theory in HOL4
by: Zhiping Shi, et al.
Published: (2013-01-01) -
Formal verification of device driver monitors in HOL 4
by: Möre, Tomas
Published: (2021)