How does the ASTREE analyzer deal with digital filters?


August 16, 2007


Jerome Feret


Ecole Normale Superieure, Paris


The ASTREE analyzer is an abstract interpretation-based static analyzer tailored to prove the absence of run time errors (division by 0, out of bounds, overflow, null pointer dereference, …) in critical embedded synchronous software as found in earth transportation, nuclear energy, medical instrumentation and aerospace applications. Its design started in November 2001 at the Laboratoire d’Informatique of the Ecole Normale Superieure (LIENS). The ASTREE analyzer was able to prove fully automatically the absence of any run time error in flight control software of fly-by-wire systems.

One particularity of the ASTREE analyzer is that it is domain-aware: it knows facts about application domains that are necessary to make sophisticated proofs. One example is the use of specific abstract domains to deal with digital filters. Digital filters are widely used in control/command programs: a digital filter is a numerical algorithm to smooth variations of sampled values of signal. Digital filters involve linear recursions that can hardly be bound by using linear invariants. In contrast, our abstract domains detect digital filters and use both quadratic constraints and formal expansion to bound the ranges of variables in digital filters.

In this talk, we will give a short summary of the ASTREE analyzer: we will briefly explain its structure and shortly describe its main abstract domains. Then we will describe the specific framework that deals with digital filtering.


Jerome Feret

Dr. Jerome Feret is a postdoctoral research fellow in the Ecole Normale Superieure, Paris, France. He is interested in abstract interpretation, mobile systems, embedded systems, static analysis and verification. He received a Ph.D. in computer science from the Ecole Polytechnique in February 2005, under the direction of Prof. Patrick Cousot. He belongs to the ASTREE project since its beginning in November 2001.