Incremental Verification by Abstraction
Verification by abstraction is a major technique for verifying
infinite-state and very large systems. This technique consists in
finding an abstraction relation and an abstract system that simulates
the concrete one and that is amenable to algorithmic verification.
One then checks that the abstract system satisfies an abstract version
of the property of interest. Well established preservation results
allow then to deduce for a large class of properties that the concrete
system satisfies the concrete property, if the abstract system
satisfies the abstract one.
In order for this technique to be used more widely, automatic
techniques are needed for 1) finding an accurate abstraction relation
and 2) automatically generating an abstract property and an abstract
system that simulates the concrete one.
In this talk, I will present a methodology for constructing
abstractions and refining them by analyzing counter-examples. I 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.
Place: Information technology, Uppsala University
Help on how to find ASTEC Seminars.
There will be an extended period for discussions after the seminar.
Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 16.00.
Everyone is welcome !
Updated 02-Mar-2001 10:57 by Roland Grönroos
e-mail: info -at- astec.uu.se