@proceedings {AFJV08,
	title = {Using Datalog and Boolean Equation Systems for Program Analysis},
	journal = {Proceedings of the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS{\textquoteright}08)},
	volume = {5596},
	year = {2009},
	pages = {215{\textendash}231},
	publisher = {Springer-Verlag},
	abstract = {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.},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva},
	editor = {Darren Cofer and Alessandro Fantechi}
}
