Concrete Model Checking with Abstract Matching and Refinement

Radek Pelanek
Faculty of Informatics, Masaryk University Brno.

The talk is based on CAV'05 paper with Corina Pasareanu and Wille Visser.

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.

Everyone is welcome !

Updated 06-Apr-2005 09:37 by Roland Grönroos
e-mail: info -at-    Location: