Generating tests from counterexamples

被引：122

作者：

Beyer, D ^{[1
]}

Chlipala, AJ ^{[1
]}

Henzinger, TA ^{[1
]}

Jhala, R ^{[1
]}

Majumdar, R ^{[1
]}

机构：

[1] Univ Calif Berkeley, Berkeley, CA 94720 USA

来源：

ICSE 2004: 26TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS | 2004年

关键词：

D O I：

10.1109/ICSE.2004.1317455

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test-vector generation is fully automatic (no user intervention) and exact (no false positives).

引用

页码：326 / 335

页数：10

共 32 条

[1]

Aho Alfred V., 1986, ADDISON WESLEY SERIE

[2]

[Anonymous], 2002, C COMPUTER COMMUNICA, DOI DOI 10.1145/586110.586142

[3]

[Anonymous], ART SOFTWARE TESTING

[4]

BALL T, 2002, POPL, P1

[5]

BODIK R, 1997, P ACM SIGPLAN 97 C P, P146

[6]

BOYAPATI C, 2002, P INT S SOFTW TEST A, P123, DOI DOI 10.1145/566172.566191

[7] Modular verification of software components in C [J].

Chaki, S ;

Clarke, E ;

Groce, A ;

Jha, S ;

Veith, H .

25TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2003, :385-395

[8]

Chen H, 2002, USENIX ASSOCIATION PROCEEDINGS OF THE 11TH USENIX SECURITY SYMPOSIUM, P171

[9]

Clarke L. A., 1981, Program flow analysis. Theory and applications, P264

[10]

Clarke L. A., 1976, IEEE Transactions on Software Engineering, VSE-2, P215, DOI 10.1109/TSE.1976.233817

← 1 2 3 4 →