Inferring Class Invariants in object-oriented languages via abstract interpretation

February 15, 2005
Francesco Logozzo | Ecole Polytechnique, Palaiseau, France

In this talk we present a static analysis, based on abstract interpretation, for the automatic inference of class invariants in Object-oriented languages. Intuitively, a class invariant is a property valid for each instantiation of a class, before and after the execution of any class method. Class invariants are important for the modular verification, the optimization and the specification of object-oriented languages. We present a generic approach for the inference of class invariants that is sound (in that it overapproximates the class semantics), generic (in that any abstract domain can be plugged-in), and modular (with respect to the instantiation context and inheritance). We will illustrate our results with several examples and using an incremental approach: we start by showing how to infer class invariants for a minimal object-oriented language, then we will consider aliasing, inheritance and mutual recursive classes.

Speaker Details

Dr. Francesco Logozzo is a postdoc researcher in the Ecole Polytechnique, Palaiseau, France. His main interestes are abstract interpretation, object-oriented programming, static analysis and verification. He received the Ph.D. in computer science from Ecole Polytechnique in June 2004, under the direction of Dr. Radhia Cousot. He is a former student of Scuola Normale Superiore, Pise, Italy.