In this thesis we propose an abstraction based certification technique for Java programs which is based on rewriting logic, 
a very general logical and semantic framework efficiently implemented in the functional programming language Maude. 
We focus on safety properties, i.e. properties of a system that are defined in terms of certain events not happening, 
which we characterize as unreachability problems in rewriting logic. The safety policy is expressed in the style of JML, 
a standard property specification language for Java modules. 
In order to provide a decision procedure, we enforce finite-state models of programs by using abstract interpretation. 
Starting from a specification of the Java semantics written in Maude, we develop an abstraction based, 
finite-state operational semantics also written in Maude  which is appropriate for program verification. 
As a by-product of the  verification based on abstraction, a dependable safety certificate is delivered which consists of 
a set of  rewriting proofs that can be easily checked by the code consumer by using a standard rewriting logic engine. 
The abstraction based proof-carrying code technique, called JavaPCC, has been implemented and successfully tested on several examples, 
which demonstrate the feasibility of our approach.

We analyse local properties of Java methods: i.e. properties of methods regarding their parameters and results. 
 We also study global confidentiality properties of complete Java  classes, 
 by initially considering non--interference and, then, erasure with and without non--interference. 
Non--interference is a semantic program property that assigns confidentiality levels to data objects 
and prevents illicit information flows from occurring from high to low security levels. 
In this thesis, we present a novel security model for global non--interference which approximates non--interference as a safety property. 
Erasure is a way of strengthening confidentiality by upgrading data confidentiality levels, 
up to the extreme of demanding the removal of secret data from the system. 
In this thesis, we also propose a certification technique for confidentiality of complete Java classes 
that includes non--interference and erasure policies.