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, mo del-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. © Springer-Verlag Berlin Heidelberg 2001.
Cite
CITATION STYLE
Lakhnech, Y., Bensalem, S., Berezin, S., & Owre, S. (2001). Incremental verification by abstraction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2031 LNCS, pp. 98–112). Springer Verlag. https://doi.org/10.1007/3-540-45319-9_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
