Abstract
We present an Abstract Interpretation-based framework for automatically analyzing programs containing digital filters. Our framework allows refining existing analyses so that they can handle given classes of digital filters. We only have to design a class of symbolic properties that describe the invariants throughout filter iterations, and to describe how these properties are transformed by filter iterations. Then, the analysis allows both inference and proofs of the properties about the program variables that are tied to any such filter.
This work was partially supported by the ASTRÉE RNTL project.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. PLDI 2003. ACM Press, New York (2003)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL 1977. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of logic and computation 2(4) (August 1992)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978. ACM Press, New York (1978)
Karr, M.: Affine relationships among variables of a program. Acta Inf. (1976)
Lamb, A.A., Thies, W., Amarasinghe, S.P.: Linear analysis and optimisation of stream programs. In: Proc. PLDI 2003. ACM Press, New York (2003)
Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system, documentation and user’s manual. Technical report, INRIA (2002)
Miné, A.: The octagon abstract domain. In: Proc. WCRE 2001(AST 2001). IEEE, Los Alamitos (2001)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Feret, J. (2004). Static Analysis of Digital Filters. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive