@inproceedings{8eb6ef8d516a4cb4ac329e575892c365,
title = "SimpleCAR: An efficient bug-finding tool based on approximate reachability",
abstract = "We present a new safety hardware model checker SimpleCAR that serves as a reference implementation for evaluating Complementary Approximate Reachability (CAR), a new SAT-based model checking framework inspired by classical reachability analysis. The tool gives a “bottom-line” performance measure for comparing future extensions to the framework. We demonstrate the performance of SimpleCAR on challenging benchmarks from the Hardware Model Checking Competition. Our experiments indicate that SimpleCAR is particularly suited for unsafety checking, or bug-finding; it is able to solve 7 unsafe instances within 1 h that are not solvable by any other state-of-the-art techniques, including BMC and IC3/PDR, within 8 h. We also identify a bug (reports safe instead of unsafe) and 48 counterexample generation errors in the tools compared in our analysis.",
author = "Jianwen Li and Rohit Dureja and Geguang Pu and Rozier, \{Kristin Yvonne\} and Vardi, \{Moshe Y.\}",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2018.; 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 14-07-2018 Through 17-07-2018",
year = "2018",
doi = "10.1007/978-3-319-96142-2\_5",
language = "英语",
isbn = "9783319961415",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "37--44",
editor = "Georg Weissenbacher and Hana Chockler",
booktitle = "Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",
address = "德国",
}