Abstract Interpretation, Static Program Analysis, Language-based Security, Information Flow, Type Systems, Functional Languages, Proof-Carrying Code, Program Slicing, Cost Analysis, Termination Analysis, Java Bytecode.

Study of Information Flow properties of programs, particularly Abstract Non-Interference \cite{plid04,tlca05,sac06,ictcs07}. Algorithms and techniques for checking Abstract Non-Interference in Imperative, Object-Oriented and Functional programming languages. Application to Proof-Carrying code architectures in order to statically obtain security certificates for programs. Study of Abstract Dependencies and their relation with Information Flow and Program Slicing \cite{pepm08}, semantic definition of Abstract Program Slicing \cite{plid08,scam08,scam08-tr}. Cost and Termination Analysis of Java Bytecode \cite{esop07,cajvm-tr,bytecode07,wst07,prole07,plid07,sac08,bytecode08,fmoods08,fmco07,ecoop-ws08}, construction of a realistic cost model, implementation of an analyzer for this task.