# Footnotes

- (1)
- The architecture of the tool allows
to replace an abstract domain for some datatype by another one; for
instance, polyhedra could be replaved by octagons. It is also
possible to add a new datatype, provided that an abstract domain for
it is available (and implemented !).
- (2)
- The classical method for verifying such systems is (was)
to enumerate all possible valuations of Boolean variables, and to
attach a numerical invariant (e.g., a polyhedra) to each of these
valuations. However this method is strongly limited by the number
of Boolean variables, which can be several dozens even for small
LUSTRE programs. Our notion of control structure induces this
method as a particular case.
- (3)
- Our control structure are quite similar to the ones otaine
by predicate abstraction; they are slightly more general and
'`surtout" are used to solve fixpoint equations on an infinite
domain, instead of being explored as a finite graph. So the result
is "this subset of states in this location may be reachable"
instead of "no state, or all states in this location may be
reachable".

Bertrand Jeannet, February 10, 2011