---

Incremental Verification by Abstraction

• Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, and Sam Owre
• Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001

---

Abstract

We present a methodology for constructing abstractions and refining them by analyzing counter-examples. We also present a uniform verification method that combines abstraction, model-checking and deductive verification in a novel way. In particular, it allows and shows how to use the set of reachable states of the abstract system in a deductive proof even when the abstract model does not satisfy the specification and when it simulates the concrete system with respect to a weaker simulation notion than Milner's.

gzipped postscript or postscript or PDF

BibTeX Entry

@INPROCEEDINGS{Lachnech-etal:TACAS01,
	AUTHOR = {Yassine Lakhnech and Saddek Bensalem and Sergey Berezin and Sam Owre},
	TITLE = {Incremental Verification by Abstraction},
	PAGES = {98--112},
	BOOKTITLE = {Tools and Algorithms for the Construction and Analysis of Systems:
		7th International Conference, {TACAS} 2001},
	YEAR = 2001,
	EDITOR = {T. Margaria and W. Yi},
	PUBLISHER = {Springer-Verlag},
	ADDRESS = {Genova, Italy},
	MONTH = apr,
	VOLUME = 2031,
	SERIES = lncs
}

---

Sam Owre: owre@csl.sri.com