Abstract matching for software model checking

被引：0

作者：

de la Cámara, P ^{[1
]}

del Mar Gallardo, M ^{[1
]}

Merino, P ^{[1
]}

机构：

[1] Univ Malaga, E-29071 Malaga, Spain

来源：

MODEL CHECKING SOFTWARE, PROCEEDINGS | 2006年 / 3925卷

关键词：

state explosion; model extraction; static analysis;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Current research in software model checking explores new techniques to handle the storage of visited states (usually called the heap). One approach consists in saving only parts or representations of the states in the heap. This paper presents a new technique to implement sound abstract matching of states. This kind of matching produces a reduction in the number of states and traces explored. With the aim of obtaining a useful result, it is necessary to establish some correctness conditions on the matching scheme. In this paper, we use static analysis to automatically construct an abstract matching function which depends on the program and the property to be verified. The soundness of the static analysis guarantees the soundness of verification. This paper describes the overall technique applied to Spin, the correctness issues and some examples which show its efficiency.

引用

页码：182 / 200

页数：19

共 11 条

[1]

BOSNACKI D, 2001, THESIS EINDHOVEN U T

[2]

Clarke E, 2001, Model checking

[3]

Corbett J. C., 2000, Proceedings of the 2000 International Conference on Software Engineering. ICSE 2000 the New Millennium, P439, DOI 10.1109/ICSE.2000.870434

[4]

DELACAMARA P, 2005, FMICS 05, P17, DOI DOI 10.1145/1081180.1081184

[5] A generalized semantics of PROMELA for abstract model checking [J].