B. Akbarpour and S. Tahar, Error analysis of digital lters using hol theorem proving, Selected papers from the 4th International Workshop on Computational Models of Scientic Reasoning and Applications, p.666, 2007.

T. Hilaire and B. Lopez, Reliable implementation of linear lters with xed-point arithmetic, Proc. IEEE Workshop on Signal Processing Systems (SiPS), 2013.

B. Akbarpour, S. Tahar, and A. Dekdouk, Formalization of xed-point arithmetic in HOL, Formal Methods in System Design, vol.27, issue.1, p.173200, 2005.

J. Park, M. Pajic, I. Lee, and O. Sokolsky, In: Scalable Verication of Linear Controller Software, p.662679, 2016.

J. Park, M. Pajic, O. Sokolsky, and I. Lee, Automatic Verication of Finite Precision Implementations of Linear Controllers, p.153169, 2017.

J. Feret, Static Analysis of Digital Filters, the 13th European Symposium on Programming -ESOP 2004, p.3348, 2004.
DOI : 10.1007/978-3-540-24725-8_4

URL : https://hal.archives-ouvertes.fr/inria-00528447

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, p.4162, 2015.
DOI : 10.1109/32.713327

URL : https://hal.archives-ouvertes.fr/hal-00860648

A. V. Oppenheim, R. W. Schafer, and J. R. Buck, Discrete-time Signal Processing, 1999.

A. Fettweiss, Wave digital lters: Theory and practice, Proc. of the IEEE, 1986.

L. Gazsi, Explicit formulas for lattice wave digital lters, IEEE Trans. Circuits & Systems, vol.32, issue.1, 1985.
DOI : 10.1109/tcs.1985.1085595

M. Palaniswami and G. Feng, Digital estimation and control with a new discrete time operator, [1991] Proceedings of the 30th IEEE Conference on Decision and Control, p.16311632, 1991.
DOI : 10.1109/CDC.1991.261682

G. Li, C. Wan, and G. Bi, An improved rho-dit structure for digital lters with minimum roundo noise, IEEE Trans. on Circuits and Systems, vol.52, issue.4, 2005.

Y. Feng, P. Chevrel, and T. Hilaire, A practical strategy of an ecient and sparse FWL implementation of LTI lters, European Control Conference

H. Hanselmann, Implementation of digital controllers???A survey, Automatica, vol.23, issue.1, p.732, 1987.
DOI : 10.1016/0005-1098(87)90115-4

M. Gevers and G. Li, Parametrizations in Control, Estimation and Filtering Probems, 1993.
DOI : 10.1007/978-1-4471-2039-1

T. Hilaire, On the transfer function error of state-space lters in xed-point context, IEEE Trans. on Circuits & Systems II, vol.56, issue.12, p.936940, 2009.

V. Balakrishnan and S. Boyd, On computing the worst-case peak gain of linear systems, Systems & Control Letters, vol.19, p.265269, 1992.

S. P. Boyd and J. Doyle, Comparison of peak and RMS gains for discrete-time systems, Systems & Control Letters, vol.9, issue.1
DOI : 10.1016/0167-6911(87)90002-8

T. Kailath, Linear Systems, 1980.

J. Lopez, C. Carreras, and O. Nieto-taladriz, Improved interval-based characterization of xed-point LTI systems with feedback loops. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, vol.26, issue.11, 2007.

S. Kim, K. Kum, and W. Sung, Fixed-point optimization utility for C and C++ based digital signal processing programs, IEEE Transactions on Circuits and Systems, vol.45, issue.11, p.14551464, 1998.

A. Volkova, T. Hilaire, and C. Q. Lauter, Reliable Evaluation of the Worst-Case Peak Gain Matrix in Multiple Precision, 2015 IEEE 22nd Symposium on Computer Arithmetic, 2015.
DOI : 10.1109/ARITH.2015.14

URL : https://hal.archives-ouvertes.fr/hal-01083879

U. Siddique, M. Y. Mahmoud, and S. Tahar, On the Formalization of Z-Transform in HOL, p.483498, 2014.
DOI : 10.1007/978-3-319-08970-6_31

T. Hilaire, P. Chevrel, and J. Whidborne, A unifying framework for nite wordlength realizations, IEEE Trans. on Circuits and Systems, vol.8, issue.54, p.17651774, 2007.
DOI : 10.1109/tcsi.2007.902408

S. Boldo and G. Melquiond, Flocq: A unied library for proving oating-point algorithms in Coq, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, p.243252, 2011.

S. Boldo and G. Melquiond, Computer Arithmetic and Formal Proofs, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632617