Analyzing Program Analyses

We want to prove that a static analysis of a given program is complete, namely, no imprecision arises when asking some query on the program behavior in the concrete (i.e., for its concrete semantics) e abstract (i.e., for its abstract interpretation). Completeness proofs are therefore useful to assign confidence to alarms raised by static analyses. We introduce the completeness class of an abstracthe set of all programs for which the abstraction is complete. Our first result shows that for any nontrivial abstraction, its completeness class is not recursively enumerable. We then introduce a stratified deductive system A to prove the completeness of prolyses over an abstract domain A. We prove the soundness of the deductive system. We observe that the only sources of incompleteness are assignments and Boolean tests — unlikely a common belief in static analysis, joins do not induce incompleteness. The ayer of this proof system is generic, abstraction-agnostic, and it deals with the ...

• Type: Journal
• Year: 2015
• Where: POPL
• Authors: Roberto Giacobazzi, Francesco Logozzo, Francesco Ranzato
• Keywords: POPL 2015, Programming Languages