Inferring Class Invariants in object-oriented languages via abstract interpretation

Опубликовано 6 сентября 2016, 5:21

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.