Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering

Document Type

Conference Proceeding

Conference

International Conference on Computer Aided Verification

Publication Version

Published Version

Publication Date

7-18-2018

Journal or Book Title

Lecture Notes in Computer Science

Volume

10982

First Page

37

Last Page

44

DOI

10.1007/978-3-319-96142-2_5

Conference Title

International Conference on Computer Aided Verification

Conference Date

July 14-17, 2018

City

Oxford, United Kingdom

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 International Conference on Computer Aided Verification 10982 (2018): 37-44. DOI: 10.1007/978-3-319-96142-2_5. Posted with permission.

Creative Commons License

Creative Commons Attribution 4.0 License
This work is licensed under a Creative Commons Attribution 4.0 License.

Copyright Owner

The Authors

Language

en

File Format

application/pdf

Share

Article Location

 
COinS