Analyzing Program Analyses

8 years 11 days ago

Download www.math.unipd.it

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 conﬁdence 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 ﬁrst result shows that for any nontrivial abstraction, its completeness class is not recursively enumerable. We then introduce a stratiﬁed 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 ...

Roberto Giacobazzi, Francesco Logozzo, Francesco R

Real-time Traffic