@TechReport{ atr116,
title = {Extending {iSAT3} with {ICP}-Contractors for Bitwise Integer Operations},
author = {Karsten Scheibler and Felix Neubauer and Ahmed Mahdi and
Martin Fr{\"{a}}nzle and Tino Teige and Tom Bienm{\"{u}}ller and
Detlef Fehrer and Bernd Becker},
institution = {SFB/TR 14 AVACS},
year = {2016},
note = {ISSN: 1860-9821, http://www.avacs.org.},
number = {116},
type = {Reports of SFB/TR 14 AVACS},
abstract = {Up to now SMT-solvers addressing floating-point
arithmetic were based on bit-blasting. Quite recently,
methods based on interval constraint propagation (ICP) for
accurate reasoning over floating-point arithmetic were proposed.
One prominent use-case for such methods is automatic dead-code
detection in floating-point dominated embedded C programs.
However, C programs usually contain a mix of floating-point
arithmetic, integer arithmetic and bitwise integer operations.
Thus, adding ICP-based support for floating-point arithmetic
is not enough -- bitwise integer operations have to be supported
as well. Therefore, this report gives a detailed overview
how these operations can be handled with ICP.},
access = {open},
bibtex = {atr116.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and
Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and
Andreas Podelski},
pdf = {avacs_technical_report_116.pdf},
series = {ATR},
subproject = {T1}
}