The Top-Down Solver—An Exercise in A²I

The top-down solver TD is a convenient local generic fixpoint engine which is at the heart of static analysis frameworks such as Ciao and Goblint. Here, we show how Patrick Cousot’s idea of applying analysis to the analyzer itself allows to derive advanced versions of TD from a recursive descent fixpoint algorithm. A run of that fixpoint algorithm provides us with a trace whose dynamic analysis allows not only to identify semantic dependencies between unknowns on-the-fly, but also to choose appropriate widening/narrowing points. It is thus not only the sequence of iterates for individual unknowns which is taken into account, but the global trace of the fixpoint algorithm itself.