Title: “Logic-Based Techniques for Program Analysis and Specification Synthesis”
Speaker: Marco Feliú
Date: May 5, 2016
Time: 10:30am – 11:30am
Location: NIA Room 137
Abstract: Program analysis can benefit from logic formalisms in many ways. In my thesis, I developed different techniques aimed to improve various aspects of static program analysis using logic. This talk provides an overview of these techniques that can be classified in two different groups “declarative program analysis” and “automated inference of specifications”.
Declarative program analysis aims to improve the customization of static analyses by using declarative languages. In our case, we use the logic language Datalog to specify analyses. Nevertheless, for a declarative approach to static analysis to succeed it must be efficient and expressive. On one hand, we improved Datalog efficiency by translating it into Boolean Equation Systems and using optimized resolution strategies. On the other hand, we improved Datalog expressiveness by translating it into Rewriting Logic.
Automated inference of specifications provides specification candidates for a program. These techniques are more useful if they provide some correctness guarantees on the specifications they generate or at least a way to verify them. In our case, we have developed two different inference techniques. On one hand, we infer equational properties for the functional-logic language Curry by means of abstract interpretation. This method allows us to classify correct and approximated parts of the inferred specification. On the other hand, we infer pre/post conditions for ADT (abstract data types) programmed in a subset of the C language by using the Matching Logic verification framework.
Bio: Dr. Feliú obtained a PhD in Computer Science from the Technical University of Valencia in October 2013. His research interests include program analysis, specification synthesis and declarative languages. Since 2014 Dr. Feliú has worked as a software engineer in several companies. He enjoys programming, especially using declarative languages such as Haskell or Maude.