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