@inproceedings{westhofen2020benchmarking,
Author = {Westhofen, Lukas and Berger, Philipp and Katoen, Joost-Pieter},
Title = {Benchmarking Software Model Checkers on Automotive Code},

Year = {2020},
Pages = {133--150},
Publisher = {Springer International Publishing},
Address = {Cham},
Isbn = {978-3-030-55754-6},
Booktitle = {NASA Formal Methods},
Doi = {10.1007/978-3-030-55754-6_8},
Url = {https://link.springer.com/chapter/10.1007%2F978-3-030-55754-6_8},
type = {inproceedings},
Abstract = {This paper reports on our experiences with verifying automotive C code by state-of-the-art open source software model checkers. The embedded C code is automatically generated from Simulink open-loop controller models. Its diverse features (decision logic, floating-point and pointer arithmetic, rate limiters and state-flow systems) and the extensive use of floating-point variables make verifying the code highly challenging. Our study reveals large discrepancies in coverage - which is at most only 20% of all requirements - and tool strength compared to results from the main annual software verification competition. A hand-crafted, simple extension of the verifier CBMC with k-induction delivers results on 63% of the requirements while the proprietary BTC EmbeddedValidator covers 80% and obtains bounded verification results for most of the remaining requirements.}
}
@COMMENT{Bibtex file generated on }