2007
Predicate Abstraction with Under-Approximation Refinement
PELÁNEK, Radek; Corina PASAREANU and Willem VISSERBasic information
Original name
Predicate Abstraction with Under-Approximation Refinement
Name in Czech
Predikátová abstrakce a zjemňování dolních aproximací
Authors
PELÁNEK, Radek (203 Czech Republic, guarantor); Corina PASAREANU (642 Romania) and Willem VISSER (710 South Africa)
Edition
Logical Methods in Computer Science, Germany, Technical University of Braunschweig, 2007, 1860-5974
Other information
Language
English
Type of outcome
Article in a journal
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Germany
Confidentiality degree
is not subject to a state or trade secret
References:
RIV identification code
RIV/00216224:14330/07:00020179
Organization unit
Faculty of Informatics
UT WoS
000262497000006
Keywords in English
model checking; predicate abstraction; under-approximation
Tags
International impact, Reviewed
Changed: 23/6/2009 12:50, doc. Mgr. Radek Pelánek, Ph.D.
In the original language
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.
In Czech
Navrhujeme metodu ověřování modelů založenou na abstrakci a zjemňování dolních aproximací. Metoda nevyžaduje generování abstraktních přechodů, místo toho prochází konkrétní přechody a pouze si ukládá abstraktní verze stavů specifikované abstrakčními predikáty. S využitím nástroje pro dokazování vět se automaticky kontroluje, zda při průchodu statového prostoru dochází ke ztrátě přesnosti. Aplikace metody je ilustrována na verifikaci souběžných programů.
Links
| GP201/07/P035, research and development project |
| ||
| 1M0545, research and development project |
|