Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering, Mathematics, Virtual Reality Applications Center

Document Type

Article

Publication Version

Accepted Manuscript

Publication Date

3-14-2020

Journal or Book Title

Lecture Notes in Computer Science

Volume

12031

First Page

180

Last Page

192

DOI

10.1007/978-3-030-41600-3_12

Abstract

SAT-based techniques comprise the state-of-the-art in functional verification of safety-critical hardware and software, including IC3/PDR-based model checking and Bounded Model Checking (BMC). BMC is the incontrovertible best method for unsafety checking, aka bug-finding. Complementary Approximate Reachability (CAR) and IC3/PDR complement BMC for bug-finding by detecting different sets of bugs. To boost the efficiency of formal verification, we introduce heuristics involving intersection and rotation of the assumption literals used in the SAT encodings of these techniques. The heuristics generate smaller unsat cores and diverse satisfying assignments that help in faster convergence of these techniques, and have negligible runtime overhead. We detail these heuristics, incorporate them in CAR, and perform an extensive experimental evaluation of their performance, showing a 25% boost in bug-finding efficiency of CAR.We contribute a detailed analysis of the effectiveness of these heuristics: their influence on SAT-based bug-finding enables detection of different bugs from BMCbased checking. We find the new heuristics are applicable to IC3/PDR-based algorithms as well, and contribute a modified clause generalization procedure.

Comments

This is a post-peer-review, pre-copyedit version of an article published as Dureja, Rohit, Jianwen Li, Geguang Pu, Moshe Y. Vardi, and Kristin Y. Rozier. In Verified Software. Theories, Tools, and Experiments. Chakraborty S., Navas J. (eds). VSTTE 2019. Lecture Notes in Computer Science 12031 (2020): 180-192. DOI: 10.1007/978-3-030-41600-3_12 . Posted with permission.

Copyright Owner

Springer Nature Switzerland AG

Language

en

File Format

application/pdf

Published Version

Share

COinS