In this talk, we present two powerful, fully automated methods to
evaluate Datalog programs: the first approach transforms the Datalog
program in an implicit Boolean Equation Systems (BESs) solved by
existing general purpose verification toolboxes, such as CADP,
providing local BES resolutions with linear-time complexity; the
second approach transforms Datalog programs into Rewriting Logic and
produces an efficient rewrite system exploiting the main features of
the high-level programming language Maude. We confirm our results
experimentally by applying it to some real-world Datalog programs in
the context of object-oriented program analyses. In this context,
Datalog is used as a specification language for expressing both
complex interprocedural program analyses involving dynamically created
objects and queries.
