Correctness Kernel of Abstract Interpretations

  • Francesco Ranzato | University of Padova

In abstract interpretation-based static analysis, approximation is encoded by abstract domains. They provide systematic guidelines for designing abstract semantic functions that approximate some concrete system behaviors under analysis. It may happen that an abstract domain contains redundant information for the specific purpose of approximating a given concrete semantic function. We introduce the notion of correctness kernel of abstract interpretations, a methodology for simplifying abstract domains, i.e. removing abstract values from them, in a maximal way while retaining exactly the same approximate behavior of the system under analysis. We show that in abstract model checking correctness kernels provide a simplification paradigm of the abstract state space that is guided by examples, meaning that this simplification preserves spuriousness of examples (i.e., abstract paths). In particular, we show how correctness kernels can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology.

Speaker Bios

Francesco Ranzato received the Laurea degree cum laude in Mathematics and the Ph.D. in Computer Science, both at the University of Padova, Italy. He visited multiple times the Laboratoire d’Informatique of Ecole Polytechnique, Palaiseaux, France, and the Computer Science Department of Ecole Normale Superieure, Paris, France. He is currently an associate professor in Computer Science at the University of Padova. His research interests include abstract interpretation, static program analysis, semantics of programming languages, automatic verification by model checking, behavioural equivalences in process algebras, lattice theory. In these areas: he has been member of program committees of international conferences and organizer of international workshops, he has been invited speaker at international workshops and at international research institutes, he has been teacher of PhD courses, he has been oprincipal investigator of a number of research projects.

Taille: Microsoft Research Talks