Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

7

CAV
2007
Springer

favoriteEmaildiscussreport

118views Hardware» more CAV 2007»

C32SAT: Checking C Expressions

13 years 10 months ago

C32SAT: Checking C Expressions

Download fmv.jku.at

C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisﬁed, is tautological, or always deﬁned 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 undeﬁned values. Under-approximation is used as optimization.

Robert Brummayer, Armin Biere

Real-time Traffic

C32SAT’s Functional Representation | CAV 2007 | Formal Methods | ISO C99 Standard | Nonportable Expressions |

claim paper

Related Content

» Type Checking C Template Instantiation by Graph Programs

» LEESA Embedding Strategic and XPathLike Object Structure Traversals in C

» A Language Framework for Expressing Checkable Properties of Dynamic Software

» Checking consistency of C and Verilog using predicate abstraction and induction

» Behavioral consistency of C and verilog programs using bounded model checking

» Checking determinism of XML Schema content models in optimal time

» Model Checking for Verification of Mandatory Access Control Models and Properties

» Unifying type checking and property checking for lowlevel code

» A Portable CompilerIntegrated Approach to Permanent Checking

Post Info
More Details (n/a)

Added	07 Jun 2010
Updated	07 Jun 2010
Type	Conference
Year	2007
Where	CAV
Authors	Robert Brummayer, Armin Biere

Comments (0)