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.
Available at: http://works.bepress.com/kristin-yvonne-rozier/44/
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.