Making abstract models complete

摘要

Completeness is a key feature of abstract interpretation. It corresponds to exactness of thernabstraction of fix-points and relies upon the need of absence of false alarms in staticrnprogram analysis. Making abstract interpretation complete is therefore a major problem inrnapproximating the semantics of programming languages. In this paper, we consider thernproblem of making abstract interpretations complete by minimally modifying the predicaterntransformer, i.e. the semantics, of a program. We study the mathematical properties ofrncomplete functions on complete lattices and prove the existence of minimal transformationsrnof monotone functions to achieve completeness. We then apply minimal completerntransformers to prove the minimality of standard program transformations in security, suchrnas static program monitoring.