In this paper we propose an abstract certification technique for Java which is based on rewriting logic, a very general logical and semantic framework efficiently implemented in the functional programming language Maude. Starting from a specification of the Java semantics written in Maude, we develop an abstract, finite-state operational semantics also written in Maude which is appropriate for program verification. As a by-product of the abstract verification, a dependable safety certificate is delivered which consists of a set of (abstract) rewriting proofs that can be easily checked by the code consumer using a standard rewriting logic engine. Our certification methodology extends to other programming languages by simply replacing the concrete semantics of Java by a semantics for the programming language at hand. The abstract proof-carrying code technique has been implemented and successfully tested on several examples, which demonstrate the feasibility of our approach.