Towards parallel program verification

被引：0

作者：

He, Pei ^{[1
]}

Kang, Lishan ^{[1
]}

机构：

[1] Wuhan Univ, State Key Lab Software Engn, Wuhan 430072, Hubei, Peoples R China

来源：

DCABES 2007 Proceedings, Vols I and II | 2007年

关键词：

program verification; parallel verification; Hoare's logic; model checking; finite state automaton;

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Parallel verification of programs is a relatively new research area. In this paper, we first introduce our modeling approach to Hoare's logic, and then present an algorithm for parallel verification. The result indicates: Hoare's logic and model checking techniques can be thoroughly combined within finite state automatons. Besides, the obtained model has a potential for parallel verification of programs over arbitrary granularity.

引用

页码：14 / 18

页数：5

共 24 条

[1]

Aho Alfred V., 1986, COMPILERS PRINCIPLES

[2]

BECKERT B, 2004, P 2 INT C SOFTW ENG

[3] Divisible task scheduling - Concept and verification [J].

Blazewicz, J ;

Drozdowski, M ;

Markiewicz, M .

PARALLEL COMPUTING, 1999, 25 (01) :87-98

[4]

Bouajjani A, 2001, LECT NOTES COMPUT SC, V2076, P24

[5] Introductory paper [J].

Luboš Brim ;

Orna Grumberg .

International Journal on Software Tools for Technology Transfer, 2005, 7 (1) :1-3

[6]

Dijkstra E. W, 1976, A Discipline of Programming

[7]

EDMUND M, 1996, ACM COMPUT SURV, V28, P626

[8]

GARAVEL H, 2001, LNCS, V2057, P217

[9]

GERARD J, 2001, VERIFICATION RELIABI, V11, P65

[10] A scalable parallel algorithm for reachability analysis of very large circuits [J].

Heyman, T ;

Geist, D ;

Grumberg, O ;

Schuster, A .

FORMAL METHODS IN SYSTEM DESIGN, 2002, 21 (03) :317-338

← 1 2 3 →