Other formats:
BibTeX
LaTeX
RIS
@article{713628,
author = {Pelánek, Radek and Pasareanu, Corina and Visser, Willem},
article_location = {Germany},
article_number = {1},
keywords = {model checking; predicate abstraction; under-approximation},
language = {eng},
issn = {1860-5974},
journal = {Logical Methods in Computer Science},
title = {Predicate Abstraction with Under-Approximation Refinement},
url = {http://www.lmcs-online.org},
volume = {3},
year = {2007}
}
TY - JOUR
ID - 713628
AU - Pelánek, Radek - Pasareanu, Corina - Visser, Willem
PY - 2007
TI - Predicate Abstraction with Under-Approximation Refinement
JF - Logical Methods in Computer Science
VL - 3
IS - 1
SP - 1-22
EP - 1-22
PB - Technical University of Braunschweig
SN - 18605974
KW - model checking
KW - predicate abstraction
KW - under-approximation
UR - http://www.lmcs-online.org
N2 - 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.
ER -
PELÁNEK, Radek, Corina PASAREANU and Willem VISSER. Predicate Abstraction with Under-Approximation Refinement. \textit{Logical Methods in Computer Science}. Germany: Technical University of Braunschweig, vol.~3, No~1, p.~1-22. ISSN~1860-5974. 2007.
|
