Title

Intersection and Rotation of Assumption Literals Boosts Bug-Finding

Campus Units

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

Document Type

Conference Proceeding

Conference

Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)

Publication Version

Accepted Manuscript

Link to Published Version

https://doi.org/10.1007/978-3-030-41600-3_12

Publication Date

3-14-2020

Journal or Book Title

Verified Software. Theories, Tools, and Experiments

First Page

180

Last Page

192

DOI

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

Conference Title

Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)

Conference Date

July 13-14, 2019

City

New York, New York

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 BMC-based 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 a conference proceeding published as Dureja, Rohit, Jianwen Li, Geguang Pu, Moshe Y. Vardi, and Kristin Y. Rozier. "Intersection and Rotation of Assumption Literals Boosts Bug-Finding." In Verified Software. Theories, Tools, and Experiments 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers. Supratik Chakraborty and Jorge A. Navas, editors. Lecture Notes in Computer Science 12031 (2020): 180-192. The final authenticated version is available online at 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

Article Location

 
COinS