Using Datalog and Boolean Equation Systems for Program Analysis

摘要

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.