CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishIn 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.
| Titolo: | Completeness Refinement in Abstract Symbolic Trajectory Evaluation | |
| Autori: | ||
| Data di pubblicazione: | 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. | |
| Handle: | http://hdl.handle.net/11562/20687 | |
| ISBN: | 9783540227915 | |
| Appare nelle tipologie: | 04.01 Contributo in atti di convegno |
File in questo prodotto:
http://hdl.handle.net/11562/20687
Copyright © 2021