C32SAT: Checking C Expressions.

Armin Biere; Robert Brummayer

C32SAT: Checking C Expressions.

Armin Biere
, Robert Brummayer

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is autological, 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 C32SATs functional representation and the way it handles undefined values. Under-approximation is used as optimization.

Original language	English
Title of host publication	19th Intl. Conf. on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science (LNCS)
Publisher	Springer
Number of pages	4
Volume	vol. 4590
Publication status	Published - 2007

Fields of science

102 Computer Sciences

Cite this

@inproceedings{6a6941a567ce4ff086acf54fde7a8cef,

title = "C32SAT: Checking C Expressions.",

abstract = "C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is autological, 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 C32SATs functional representation and the way it handles undefined values. Under-approximation is used as optimization.",

author = "Armin Biere and Robert Brummayer",

year = "2007",

language = "English",

volume = "vol. 4590",

booktitle = "19th Intl. Conf. on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

}

TY - GEN

T1 - C32SAT: Checking C Expressions.

AU - Biere, Armin

AU - Brummayer, Robert

PY - 2007

Y1 - 2007

N2 - C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is autological, 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 C32SATs functional representation and the way it handles undefined values. Under-approximation is used as optimization.

AB - C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is autological, 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 C32SATs functional representation and the way it handles undefined values. Under-approximation is used as optimization.

M3 - Conference proceedings

VL - vol. 4590

BT - 19th Intl. Conf. on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science (LNCS)

PB - Springer

ER -