Completeness Refinement in Abstract Symbolic Trajectory Evaluation

In this paper we study the relation between the lack of completeness in abstract symbolic trajectory evaluation and the structure of the counterexamples that can be derived in case of property failure. We characterize the presence of false negatives as a loss of completeness of the underlying abstraction. We prove how standard completeness refinement in abstract interpretation provides a systematic way for refining abstract symbolic trajectory evaluation in order to gain completeness for the properties of interest.