We present a logic for the specification of static analysis problems that goes beyond the logics traditionally used. Its most prominent feature is the direct support for both inductive computations of behaviors as well as co-inductive specifications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worst case time complexity result. We show that the logic and the associated solver can be used for rapid prototyping of analyses and illustrate a wide variety of applications within Static Analysis, Constraint Satisfaction Problems and Model Checking. In all cases the complexity result specializes to the worst case time complexity of the classical methods.
Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming, 2012, p. 45-54
Static analysis; Model checking; Abstract interpretation
Main Research Area:
14th International Symposium on Association for Computing Machinery Principles and Practice of Declarative Programming (PPDP 2012)Principles and Practice of Declarative Programming