@inproceedings{BGL03,
title = { Abstraction as the Key for Invariant Verification },
author = {Bensalem, Saddek and Graf, Susanne and Lakhnech, Yassine},
year = {2003},
booktitle = {Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday},
pages = {67-99},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2772},
team = {DCS},
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 particular, we show how to use the abstract system in a deductive proof even when the abstract model does not satisfy the specification but simulates the concrete system with respect to a weaker notion of simulation than Milner's.},
}
