25th MBMV Workshop
Date: February 17th, 2022
BTC Embedded Systems will join the 25th MBMV Workshop and give a talk about "Detection and Elimination of Constants to Strengthen k-Induction"
Please find more information about the event here.
"Detection and Elimination of Constants to Strengthen k-Induction"
Presenter: Lukas Mentel
During the last years, software model checking has become a reliable
technique for the verification of software that is used in
safety-critical environments -- e.g. to prove the absence of dead code.
One technique to perform such proofs is k-induction which considers in
its induction step the property and transition relation but ignores the
initial states. Therefore, k-induction is very sensitive regarding the
encoding of variables which have a constant value -- in particular if
the encoding depends on the initial states. A recent bachelor thesis
addresses this problem. In this paper, we present the main results,
describe the integration into the commercial test and verification tool
BTC EmbeddedPlatform(R) and evaluate our implementation on a benchmark
set with verification tasks originating from the automotive domain.