Current

Quantitative Analysis of Computational Resources (QACR) [April 2004 - March 2007]

Investigation of the role of resources in computing from a programming language point of view. Focus on access, availability and comsumption of resources.

A Three-valued Model Checker for C Programs [Oct. 2004 - Sept. 2007]

Extending Microsoft Research's model checker SLAM with sound predicate abstractions for properties that mix path quantifiers. Developing optimizations that combat the loss of precision inherent in such extensions.

Program Analysis and the Typed Pi-Calculus: Foundations and Applications to Security.

The project's web page .
We investigate the feasibility of using the Pi-calculus as a general foundation of PA technologies. We choose qualitative and quantitative Information Flow Analysis as a concrete domain in which we experiment our thesis.

Completed

Probabilistic Abstract Interpretation. (PAI)

Development of an abstract interpretation methodology based on a probabilistic semantics utilising as the semantical domains linear spaces. This new methodology allows us to consider the concept of a closest approximations.

Secure and Safe Systems ( SECSAFE ) [Nov. 2000-Oct. 2003]

Application of program analyisis techniques to the validation of security and safety aspects of realistic programming languages. In particular, the project focused a substantial part of its efforts on the development of techniques for the analysis of Java Card applications (bytecode).