Using dynamic symbolic execution to improve deductive verification

被引：0

作者：

Vanoverberghe, Dries ^{[1
]}

Bjorner, Nikolaj ^{[1
]}

de Halleux, Jonathan ^{[1
]}

Schulte, Wolfram ^{[1
]}

Tillmann, Nikolai ^{[1
]}

机构：

[1] Microsoft Res, Redmond, WA 98052 USA

来源：

MODEL CHECKING SOFTWARE, PROCEEDINGS | 2008年 / 5156卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

One of the most challenging problems in deductive program verification is to find inductive program invariants typically expressed using quantifiers. With strong-enough invariants, existing provers can often prove that a program satisfies its specification. However, provers by themselves do not find such invariants. We propose to automatically generate executable test cases from failed proof attempts using dynamic symbolic execution by exploring program code as well as contracts with quantifiers. A developer can analyze the test cases with a traditional debugger to determine the cause of the error; the developer may then correct the program or the contracts and repeat the process.

引用

页码：9 / 25

页数：17

共 35 条

[1]

Anand S, 2008, LECT NOTES COMPUT SC, V4963, P367, DOI 10.1007/978-3-540-78800-3_28

[2] Zap: Automated theorem proving for software analysis [J].

Ball, T ;

Lahiri, SK ;

Musuvathi, M .

LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 :2-22

[3]

BARNETT M, 2004, LNCS, V3362, P49, DOI [DOI 10.1007/978-3-540-30569-9_3, 10.1007/978-3-540-30569-9_3, 10.1007]

[4]

Barrett C, 2007, LECT NOTES COMPUT SC, V4590, P298

[5]

Cadar C., 2006, CCS '06: Proceedings of the 13th ACM conference on Computer and communications security, New York, NY, USA, P322

[6]

Cheon Y, 2002, LECT NOTES COMPUT SC, V2374, P231

[7]

CHEON Y, 2007, AUTOMATED RANDOM TES

[8]

CHEON Y, 2003, 0309 IOW STAT U DEP

[9]

Ciupa I., 2007, ISSTA 07, P84, DOI [10.1145/1273463.1273476, DOI 10.1145/1273463.1273476]

[10]

Ciupa I, 2008, ICSE'08 PROCEEDINGS OF THE THIRTIETH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, P71, DOI 10.1145/1368088.1368099

← 1 2 3 4 →