Abstraction and Refinement in Static Model-Checking

Details Abstraction and Refinement in Static Model-Checking Abstraction and Refinement in Static Model-Checking

2009-02-11

arxiv.org/abs/0902.1871v1

IEEE-Computer Society International Conference on Computer Science and Information Technology, ICCSIT-2008 (2008) 107 - 112

Computer Science

Data Structures and Algorithms

Scientific paper

interpretation is a general methodology for building static analyses of programs. It was introduced by P. and R. Cousot in \cite{cc}. We present, in this paper, an application of a generic abstract interpretation to domain of model-checking. Dynamic checking are usually easier to use, because the concept are establishe d and wide well know. But they are usually limited to systems whose states space is finite. In an other part, certain faults cannot be detected dynamically, even by keeping track of the history of the states space.Indeed, the classical problem of finding the right test cases is far from trivial and limit the abilities of dynamic checkers further. Static checking have the advantage that they work on a more abstract level than dynamic checker and can verify system properties for all inputs. Problem, it is hard to guarantee that a violation of a modeled property corresponds to a fault in the concrete system. We propose an approach, in which we generate counter-examples dynamically using the abstract interpretation techniques.

Affiliated with

Also associated with

No associations

Rating

Abstraction and Refinement in Static Model-Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Abstraction and Refinement in Static Model-Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Abstraction and Refinement in Static Model-Checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-487753