This paper describes a
powerful, fully automated method to evaluate Datalog queries by using
Boolean Equation Systems (Bess), and its application to object-oriented
program analysis. Datalog is used as a specification language for
expressing complex interprocedural program analyses involving
dynamically created objects. In our methodology, Datalog rules encoding
a particular analysis together with a set of constraints (Datalog facts
that are automatically extracted from program source code) are
dynamically transformed into a Bes, whose local resolution corresponds
to the demand-driven evaluation of the program analysis. This approach
allows us to reuse existing general purpose verification toolboxes,
such as Cadp, providing local Bes resolutions with linear-time
complexity. Our evaluation technique has been implemented and
successfully tested on several Java programs and Datalog analyses that
demonstrate the feasibility of our approach.