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

Thumbnail Image
Date
2018-07-18
Authors
Li, Jianwen
Dureja, Rohit
Pu, Geguang
Rozier, Kristin Yvonne
Vardi, Moshe
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Person
Rozier, Kristin Yvonne
Associate Professor
Research Projects
Organizational Units
Organizational Unit
Organizational Unit
Organizational Unit
Journal Issue
Is Version Of
Versions
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
Copyright
Mon Jan 01 00:00:00 UTC 2018