Equipe BD
Equipe BD
Laboratoire d'InfoRmatique en Images et Systèmes d'information
UMR 5205 CNRS/INSA de Lyon/Université Claude Bernard Lyon 1/Université Lumière Lyon 2/Ecole Centrale de Lyon

You are here

Using Boolean Equations and Rewriting Systems to solve Datalog Programs

Christophe Joubert
Tuesday, April 6, 2010 - 14:00 to 15:00

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.