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.

Completeness Refinement in Abstract Symbolic Trajectory Evaluation

DALLA PREDA, Mila
2004

Abstract

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.
9783540227915
Abstract Interpretation; Completeness; Domain Refinement; Symbolic Trajectory Evaluation; Verification; Model Checking; Data Flow Analysis
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/20687
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact