Computer Science – Computer Science and Game Theory
Scientific paper
2007-01-22
LMCS 3 (1:5) 2007
Computer Science
Computer Science and Game Theory
22 pages, 3 figures, accepted for publication in Logical Methods in Computer Science journal (special issue CAV 2005)
Scientific paper
10.2168/LMCS-3(1:5)2007
We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. 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. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. We illustrate the application of the approach for checking concurrent programs.
Pasareanu Corina S.
Pelanek Radek
Visser Willem
No associations
LandOfFree
Predicate Abstraction with Under-approximation Refinement 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 Predicate Abstraction with Under-approximation Refinement, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Predicate Abstraction with Under-approximation Refinement will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-205769