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


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

Publication Version

Accepted Manuscript

Link to Published Version


Publication Date


Journal or Book Title

Verified Software. Theories, Tools, and Experiments

First Page


Last Page




Conference Title

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

Conference Date

July 13-14, 2019


New York, New York


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.


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



File Format


Published Version


Article Location