DATALOG_SOLVE Tool for Static Analysis of Object-Oriented Programs

Organisation:	Universidad Politécnica de Valencia (SPAIN)
Functionality:	Static analysis.
Tools used:	CADP (Construction and Analysis of Distributed Processes) JOEQ
Period:	2008-2009
Description:	Program analysis is a technique for statically determining dynamic properties of programs. Static analysis generally executes an abstract version of the program's semantics on abstract data rather than on concrete data. Several kinds of program analyses can be formulated in Datalog, a simple relational query language that is reach enough to describe complex interprocedural program analyses involving dynamically created objects. Datalog allows, on the one hand, to formulate queries in a succinct manner (a few lines of Datalog are sufficient instead of hundreds of lines of code in a traditional language) and, on the other hand, Datalog has been extensively optimized in the field of logic programming and deductive databases. This work deals with the translation of Datalog queries into boolean equation systems (BESs), which allows to evaluate queries in a demand-driven way by using the resolution engines available in verification tools, such as the CAESAR_SOLVE library of CADP. A Datalog query is first translated into a parameterized BES, which is subsequently instantiated on-the-fly, yielding a BES which is fed to the linear-time local resolution algorithms of CAESAR_SOLVE. The translation has been implemented in the DATALOG_SOLVE tool, which takes as input the domain definitions, the Datalog constraints or facts, and a Datalog query, and produces the parameterized BES representing the problem, which is instantiated and solved using CAESAR_SOLVE. DATALOG_SOLVE has been applied to analyze JAVA programs by context-insensitive pointer analysis, a form of static analysis suitable for encoding in Datalog. Several JAVA benchmarks were handled successfully, the largest one containing 375 classes, 1531 methods, and 17000 variables.
Conclusions:	The resolution of Datalog queries by translating them into BESs and by using the linear-time BES resolution algorithms available in the CAESAR_SOLVE library of CADP allowed to build the new deductive database solver DATALOG_SOLVE in a robust and modular way. Besides the traditional applications for on-the-fly verification and state space reduction, the BES resolution technology available in CADP also proves to be useful in other areas, such as the static analysis of programs.
Publications:	[Alpuente-Feliu-Joubert-Villanueva-08] María Alpuente, Marco A.Feliú, Christophe Joubert, and Alicia Villanueva. "Using Datalog and Boolean Equation Systems for Program Analysis". Proceedings of the 13th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2008, Lecture Notes in Computer Science vol. 5596, pp. 215-231. Springer Verlag, September 2008. Full version available on-line at: http://www.dsic.upv.es/~joubert/publications/Alpuente-Feliu-Joubert-Villanueva-08-a.pdf or from the CADP Web site in PDF or PostScript [Alpuente-Feliu-Joubert-Villanueva-09] María Alpuente, Marco A.Feliú, Christophe Joubert, and Alicia Villanueva. "DATALOG_SOLVE: A Datalog-Based Demand-Driven Program Analyzer". Proceedings of the 8th Spanish Conference on Programming and Computer Languages PROLE'2008, Electronic Notes in Theoretical Computer Science vol. 248, pp. 57-66. Elsevier, August 2009. Available on line at: http://dx.doi.org/10.1016/j.entcs.2009.07.059 or from the CADP Web site in PDF or PostScript
Contact:	Christophe Joubert Technical University of Valencia / DSIC Camino de Vera s/n, 46022 Valencia SPAIN Tel: + 34 963 87 70 07 + 83516 Fax: + 34 963 87 73 59 Email: joubert@dsic.upv.es
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page