C32SAT: Checking C expressions - (Tool paper)

被引：0

作者：

Brummayer, Robert ^{[1
]}

Biere, Armin ^{[1
]}

机构：

[1] Johannes Kepler Univ Linz, Inst Formal Models & Verificat, A-4040 Linz, Austria

来源：

COMPUTER AIDED VERIFICATION, PROCEEDINGS | 2007年 / 4590卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is tautological, or always defined according to the ISO C99 standard. C32SAT can be used to detect nonportable expressions where program behavior depends on the compiler. Our contribution consists of C32SAT's functional representation and the way it handles undefined values. Under-approximation is used as optimization.

引用

页码：294 / +

页数：2

共 12 条

[1]

BIERE A, 2004, 444 NANOSAT

[2]

BIERE A, 2006, J SATISFIABILITY BOO, V2

[3]

BIERE A, UNPUB OCCURRENCE LIS

[4]

Brummayer R, 2006, P 2 DOCT WORKSH MATH

[5]

BRYANT RE, 2007, IN PRESS P TACAS 200

[6]

Clarke E, 2005, LECT NOTES COMPUT SC, V3440, P570

[7] A tool for checking ANSI-C programs [J].

Clarke, E ;

Kroening, D ;

Lerda, F .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 :168-176

[8]

Cook B, 2005, LECT NOTES COMPUT SC, V3576, P296

[9]

*ISO IEC, 1999, PROGR LANG C ISO IEC

[10] Robust Boolean reasoning for equivalence checking and functional property verification [J].

Kuehlmann, A ;

Paruthi, V ;

Krohm, F ;

Ganai, MK .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2002, 21 (12) :1377-1394

← 1 2 →