Classical Program Analysis. Program analysis offers static compile-time techniques for predicting safe and computable approximations of the run-time behaviour of a program. Abstract Interpretation is a theory for formally deriving such analyses based on the construction of (safe) non-standard semantics via the notion of Galois connections. Classical analysis techniques concentrate on the determination of qualitative aspects of programs of imperative and object oriented languages e.g. Control and Data flow analysis (flow logic) and standard type and effect systems. Examples of research in this area are recent works on information flow for sequential programming languages and the development of flow logics for the validation of security and safety properties of Java Card programs. Concurrency and the Pi-Calculus. The pi-calculus, originally developed to model concurrency, is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive : name passing. Research in this area concentrates on showing how the pi-calculus can be used for developing and justifying non-trivial type-based analyses of programming languages (data confidentiality, secure information flow, access control, etc.) and, furthermore, on showing the feasibility of using the pi-calculus as a general foundation of PA technologies. Model Checking. In model checking a program or system is captured in a mathematical model, constraints on state or behavior are expressed as a formula in a temporal logic or related language, and compliance of models with constraints is checked automatically. Such checks often are undecidable or too complex, creating the need for abstracting models, constraints or checks so that verification or refutation of compliance with constraints demonstrated in the abstract setting apply equally to the un-abstracted, non-checkable case. These efforts are informed by extant work on abstractions in program analysis and apply to quantitative and probabilistic models as well. Probabilistic Abstract Interpretation. The basic idea behind abstract interpretation is to analyse a program not in terms of its standard or concrete semantics, but rather in terms of an appropriate, simplified abstract semantics. Whereas the classical Cousot framework is based on order theoretic notions our aim is to introduce an abstract interpretation methodology based on a probabilistic semantics utilising as the semantical domains linear spaces. The result is a Probabilistic Abstract Interpretation methodology which allows us to consider the concept of a closest approximations. Security Properties. We are interested in the application and development of program analysis techniques to the validation of security properties of programs. Our research focuses on both qualitative and quantitative aspects of different security concerns - such as information flow, data confidentiality, access control, timing attacks - under several programming paradigms (imperative, object oriented, mobile and concurrent computation). We use well-established and standard techniques (control and data flow analysis, flow logics, abstract interpretation) while contributing to the state-of-the-art with new developments on type-based pi-calculus, quantitaive analysis and probabilistic abstract interpretation. Statistical and Quantitative Aspects. There are several other properties of programs which are - or at least can be seen as - of a quantitative rather than purely qualitative nature. The addition of these quantities allows for a natural formulation of the average behaviour of a program, whose specification and analysis is particularly important in the study of system performance and reliability. It also allows for an average-case analysis of programs and not just of their worst case behaviour (as it is common with classical static analysis)