Concrete Model Checking with Abstract Matching and Refinement
Faculty of Informatics, Masaryk University Brno.
The talk is based on CAV'05 paper with Corina Pasareanu and
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.
Place: Information technology, Uppsala University
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- astec.uu.se