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. ,
Reliable implementation of linear lters with xed-point arithmetic, Proc. IEEE Workshop on Signal Processing Systems (SiPS), 2013. ,
Formalization of xed-point arithmetic in HOL, Formal Methods in System Design, vol.27, issue.1, p.173200, 2005. ,
In: Scalable Verication of Linear Controller Software, p.662679, 2016. ,
Automatic Verication of Finite Precision Implementations of Linear Controllers, p.153169, 2017. ,
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
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
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
Discrete-time Signal Processing, 1999. ,
Wave digital lters: Theory and practice, Proc. of the IEEE, 1986. ,
Explicit formulas for lattice wave digital lters, IEEE Trans. Circuits & Systems, vol.32, issue.1, 1985. ,
DOI : 10.1109/tcs.1985.1085595
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
An improved rho-dit structure for digital lters with minimum roundo noise, IEEE Trans. on Circuits and Systems, vol.52, issue.4, 2005. ,
A practical strategy of an ecient and sparse FWL implementation of LTI lters, European Control Conference ,
Implementation of digital controllers???A survey, Automatica, vol.23, issue.1, p.732, 1987. ,
DOI : 10.1016/0005-1098(87)90115-4
Parametrizations in Control, Estimation and Filtering Probems, 1993. ,
DOI : 10.1007/978-1-4471-2039-1
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. ,
On computing the worst-case peak gain of linear systems, Systems & Control Letters, vol.19, p.265269, 1992. ,
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
Linear Systems, 1980. ,
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. ,
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. ,
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
On the Formalization of Z-Transform in HOL, p.483498, 2014. ,
DOI : 10.1007/978-3-319-08970-6_31
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
Flocq: A unied library for proving oating-point algorithms in Coq, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, p.243252, 2011. ,
Computer Arithmetic and Formal Proofs, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01632617