Grande Salle de VERIMAG
10 May 2010 - 10h00
Datalog-based Program Analysis with BES and RWL
by Christophe JOUBERT from Technical University of Valencia, Spain
Abstract: In this talk, we present two powerful, fully automated methods to
evaluate Datalog queries in the context of object-oriented program
analyses: 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. Datalog is used as a
specification language for expressing both complex interprocedural
program analyses involving dynamically created objects and queries. We
confirm our results experimentally by applying it to some real-world
Datalog-based analyses.
