From Numerical Transition Systems
Jump to: navigation, search

Yannis Smaragdakis, University of Athens

Declarative Static Program Analysis

We discuss the benefits of using logic-based declarative languages as a means to specify static program analysis algorithms. The main focus will be on the Doop framework for pointer analysis of Java programs. Doop encodes multiple analysis algorithms for Java declaratively, using Datalog: a logic-based language for defining (recursive) relations. The algorithms are elegantly specified and easy to understand and adapt. With an aggressive optimization methodology, Doop also achieves very high performance--often a factor of 10 faster than other comparable frameworks. With the help of Doop's concise algorithm representation we have explored several new analysis algorithms and developed important insights on existing algorithm variations.

Dino Distefano, Queen Mary University of London and Facebook

Separation Logic Static Analysis @ Facebook

In this tech talk I'll present the current activities of the Static Analysis Tool team for integrating separation logic based program analysis at Facebook. I will present the challenges we have encountered and some technical details of the solutions we have found.