SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability

Date
2018-07-18
Authors
Li, Jianwen
Dureja, Rohit
Pu, Geguang
Rozier, Kristin Yvonne
Rozier, Kristin Yvonne
Vardi, Moshe
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Aerospace Engineering
Organizational Unit
Computer Science
Organizational Unit
Journal Issue
Series
Department
Aerospace EngineeringComputer ScienceElectrical and Computer Engineering
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.

Comments

This proceeding is published as Li, Jianwen, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, and Moshe Y. Vardi. "SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability." In: Chockler H., Weissenbacher G. (eds) Computer Aided Verification. CAV 2018. Lecture Notes in Computer Science, vol 10982. (2018): 37-44. DOI: 10.1007/978-3-319-96142-2_5. Posted with permission.

Description
Keywords
Citation
DOI