We present a model-checker for boolean programs with (possibly
recursive) procedures and the temporal logic LTL. The checker is
guaranteed to terminate even for (usually faulty) programs in which
the depth of the recursion is not bounded. The algorithm uses automata
to finitely represent possibly infinite sets of stack contents and
BDDs to compactly represent finite sets of values of boolean variables.
We illustrate the checker on some examples and compare it with the
Bebop tool of Ball and Rajamani.
