ICP and IC3
Karsten Scheibler1,a, Felix Winterer2,a, Tobias Seufert2,b, Tino Teige1,b, Christoph Scholl2,c and Bernd Becker2,d
1BTC Embedded Systems AG Oldenburg, Germany
ascheibler@btc-es.de
bteige@btc-es.de
2University of Freiburg Freiburg, Germany
awinteref@informatik.uni-freiburg.de
bseufert@informatik.uni-freiburg.de
cscholl@informatik.uni-freiburg.de
dbecker@informatik.uni-freiburg.de
ABSTRACT
If embedded systems are used in safety-critical environments, they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further
Keywords: SMT, ISAT3, ICP, IC3, PDR, Software Verification.
