Abstract
At present, the usuall approach to software model checking is to use counterexample guided refinement based on predicate abstraction and over-approximation. We present a novel technique based on refinement of an under-approximation. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. Refinement generates new predicates and it is based on checking wether the abstraction introduces any loss of precision with respect to each explored transition.

ASTEC seminar
April 14, 2005

Place: Information technology, Uppsala University
Room: 1212
Time: 13.15-14.00 (+ discussions)

Room 1212 is in building 1, floor 2.

Help on how to find ASTEC Seminars.