R
A
Last name: ROLLET
First name: Antoine
International audience
This technical report provides all the source code of the Flasher Manager as well as of the test programs. The Flasher Manager is an industrial application from a car manufacturer that is embedded as a C program in a car computer. The benchmarks are based on four safety properties specified by the Flasher Manager designers.
Safety property checking is mandatory in the validation process of critical software. When formal verification tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is an important issue in practice. We investigate in this paper the capabilities of constraint-based bounded model checking for...
Safety property checking is mandatory in the validation process of critical software. When formal verification tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is an important issue in practice. We investigate in this paper the capabilities of constraint-based bounded model checking for...
International audience