DATE 2021 - Virtual Conference
1. - 5. February 2021
Location: Online (virtual conference)
In cooperation with the University of Freiburg BTC Embedded Systems extended the SMT solver iSAT3. This solver is part of BTC EmbeddedPlatform and is used, e.g., for formal verification tasks or for the automatic test generation. The results will be published as a paper on the DATE conference and Felix Winterer (University of Freiburg) will give a talk about this research collaboration on February 3rd at 17:45. The title of the paper and the talk is 'ICP and IC3'.
Please find more information on www.date-conference.com.
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.