Skip to main content
Presentation
SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability
Computer Aided Verification
  • Jianwen Li, Iowa State University
  • Rohit Dureja, Iowa State University
  • Geguang Pu, East China Normal University
  • Kristin Yvonne Rozier, Iowa State University
  • Moshe Y. Vardi, Rice University
Document Type
Conference Proceeding
Conference
30th International Conference on Computer Aided Verification
Publication Version
Published Version
Publication Date
7-18-2018
DOI
10.1007/978-3-319-96142-2_5
Conference Title
30th International Conference on Computer Aided Verification
Conference Date
July 14-17, 2018
Geolocation
(51.7520209, -1.2577263000000585)
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.

Creative Commons License
Creative Commons Attribution 4.0 International
Copyright Owner
The Authors
Language
en
File Format
application/pdf
Citation Information
Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, et al.. "SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability" Oxford, United KingdomComputer Aided Verification (2018) p. 37 - 44
Available at: http://works.bepress.com/kristin-yvonne-rozier/29/